proposition: Lemma accept_app_eq: forall s1 s2 re1 re2, s1 \in re1 -> s2 \in re2 -> (s1 ++ s2) \in re1;; re2.
proof: Proof. intros. apply accept_app with (s1:=s1) (s2:=s2); auto. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang