proposition: Corollary ka_complete_weq: forall e f, lang e ≡ lang f -> e ≡ f.
proof: Proof. intros e f. rewrite 2weq_spec. now split; apply ka_complete_leq. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation