proposition: Theorem kat_complete_weq n m: forall e f: gregex n m, G e ≡ G f -> e ≡ f.
proof: Proof. intros e f H. apply gl_weq in H. rewrite 2G_hat in H. apply ka_complete_weq in H. apply w_weq in H. rewrite 2wvo_uo in H. apply erase_faithful_weq in H. 2: now rewrite 2o_level. 2: reflexivity. apply o_inj in H. rewrite 2teval_hat in H. assumption. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms