proposition: Lemma union_inv: forall s l, s \in union l -> exists r, List.In r l /\ s \in r.
proof: Proof. induction l; intros. { simpl in *. inversion H. } simpl in *. inversion H; subst; clear H. { eauto. } apply IHl in H3. destruct H3 as (r, (Hi, Hs)). exists r; eauto. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang