proposition: Lemma o'o: forall n m (e: gregex n m), o' (o e) ≡ e.
proof: Proof. induction e; simpl o; simpl o'. reflexivity. apply o'o_pred. reflexivity. now apply cup_weq. now apply dot_weq. now apply itr_weq. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms