proposition: Theorem add_assoc' : forall n m p : nat, n + (m + p) = (n + m) + p.
proof: Proof. Admitted. Lemma re_opt_e_match'' : forall T (re: reg_exp T) s, s =~ re -> s =~ re_opt_e re. Proof. intros T re s M. induction M as [| x' | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2 | s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH | re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2]; simpl. - apply MEmpty. - apply MChar. - destruct re1; try (apply MApp; [apply IH1 | apply IH2]). inversion Hmatch1. simpl. apply IH2. - apply MUnionL. apply IH. - apply MUnionR. apply IH. - apply MStar0. - apply MStarApp; [apply IH1 | apply IH2]. Qed.
imports: Coq(Arith List) LF(IndProp)