proposition: Corollary ka_complete_leq: forall e f, lang e ≦ lang f -> e ≦ f.
proof: Proof. intros e f. rewrite <-(eval_dfa nil e), <-(eval_dfa (dfa.vars (dfa nil e)) f). apply dfa_complete_leq. lattice. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation