proposition: Lemma accept_star_eq: forall s re, s \in re -> s \in r_star re.
proof: Proof. intros s re H. destruct s. { auto using accept_star_nil. } apply accept_star_cons with (s1:=a :: s) (s2:=[]); auto using accept_star_nil, app_nil_end. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang