proposition: Lemma re_ind_eval leq weq (e: regex'): eval (X:=re_ind leq weq) (f':=fun _ =>regex_tt) var (to_expr e) = e.
proof: Proof. induction e; simpl in *; reflexivity || congruence. Qed.
imports: syntax kleene boolean lang lset sums normalisation