proposition: Corollary ka_correct_complete_leq: forall e f, lang e ≦ lang f <-> e ≦ f.
proof: Proof. split. apply ka_complete_leq. apply lang_leq. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation