proposition: Lemma napp_star : forall T m s1 s2 (re : reg_exp T), s1 =~ re -> s2 =~ Star re -> napp m s1 ++ s2 =~ Star re.
proof: Proof. intros T m s1 s2 re Hs1 Hs2. induction m. - simpl. apply Hs2. - simpl. rewrite <- app_assoc. apply MStarApp. + apply Hs1. + apply IHm. Qed.
imports: Coq(Lia)