proposition: Lemma accept_star_cons: forall s1 s2 s3 re, s1 \in re -> s2 \in r_star re -> s3 = s1 ++ s2 -> s3 \in r_star re.
proof: Proof. intros. destruct s1; simpl in *; subst. { assumption. } apply accept_star_cons_neq with (s1:=a::s1) (s2:=s2); auto. intros N; inversion N. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang