proposition: Corollary ka_weq_dec: forall e f: regex', {e ≡f} + {~(e ≡f)}.
proof: Proof. intros e f. destruct (ka_leq_dec e f). destruct (ka_leq_dec f e). left. now apply antisym. right. rewrite weq_spec. tauto. right. rewrite weq_spec. tauto. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation