proposition: Lemma re_opt_e_match : forall T (re: reg_exp T) s, s =~ re -> s =~ re_opt_e re.
proof: 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. - simpl. apply MChar. - simpl. destruct re1. + apply MApp. * apply IH1. * apply IH2. + inversion Hmatch1. simpl. apply IH2. + apply MApp. * apply IH1. * apply IH2. + apply MApp. * apply IH1. * apply IH2. + apply MApp. * apply IH1. * apply IH2. + apply MApp. * apply IH1. * apply IH2. - simpl. apply MUnionL. apply IH. - simpl. apply MUnionR. apply IH. - simpl. apply MStar0. - simpl. apply MStarApp. * apply IH1. * apply IH2. Qed.
imports: Coq(Arith List) LF(IndProp)