proposition: Corollary G_hat n m (e: gregex n m): gl (G e) ≡ R (v (o (teval (hat e)))).
proof: Proof. rewrite <-(teval_hat e) at 1. apply G_clean, clean_hat. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms