proposition: Lemma accept_app_star_skip: forall s r1 r2, s \in r2 -> s \in r_star r1;; r2.
proof: Proof. intros. apply accept_app with (s1:=[]) (s2:=s). - apply accept_star_nil. - assumption. - reflexivity. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang