proposition: Theorem clean_hat n m (e: gregex n m): clean (hat e).
proof: Proof. induction e; simpl hat. apply clean_bot. apply clean_map. intros ? _. apply clean_pred. apply clean_sup. intros ? _. apply clean_sup. intros ? _. apply clean_single, clean_elem_var. now apply clean_cup. now apply clean_dot'. apply clean_dot'. assumption. apply clean_str'. assumption. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms