proposition: Corollary kat_reduces_to_ka n m: forall e f: gregex n m, e ≡f <-> v (o (teval (hat e))) ≡ v (o (teval (hat f))).
proof: Proof. intros. split; intro H. apply ka_complete_weq. now rewrite <-2G_hat, 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. now rewrite 2teval_hat in H. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms