proposition: Corollary o_inj n m (e f: gregex n m): o e ≡ o f -> e ≡ f.
proof: Proof. intro H. apply o'_weq in H. revert H. now rewrite 2o'o. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms