proposition: Corollary kat_dec n m: forall e f: gregex n m, {e ≡f} + {~(e ≡f)}.
proof: Proof. intros. eapply sumbool_iff. symmetry. apply kat_reduces_to_ka. apply ka_weq_dec. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms