proposition: Corollary kat_correct_complete_weq n m: forall e f: gregex n m, G e ≡ G f <-> e ≡ f.
proof: Proof. split. apply kat_complete_weq. apply G.lang_weq. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms