proposition: Lemma in_union: forall l s a, List.In a l -> s \in a -> s \in union l.
proof: Proof. unfold union; induction l; intros. { contradiction. } destruct H. { subst. simpl. auto using accept_union_l. } simpl. eauto using accept_union_r. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang