proposition: Theorem teval_hat n m (e: gregex n m): teval (hat e) ≡ e.
proof: Proof. induction e; simpl hat. reflexivity. apply teval_prd. apply teval_var. setoid_rewrite sup_app. now apply cup_weq. rewrite teval_dot. now apply dot_weq. rewrite teval_dot, teval_str, <-itr_str_l. 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