proposition: Lemma in_svars_elim x : forall l, In x (svars l) -> exists y, In y l /\ In x (vars (s y)).
proof: Proof. induction l; simpl; intros. contr. ded (in_app_or H). destruct H0. exists a. auto. ded (IHl H0). do 2 destruct H1. exists x0. auto. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)