proposition: Corollary ka_correct_complete_weq: forall e f, lang e ≡ lang f <-> e ≡ f.
proof: Proof. split. apply ka_complete_weq. apply lang_weq. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation