proposition: Lemma in_svars_intro x y : forall l, In x (vars (s y)) -> In y l -> In x (svars l).
proof: Proof. induction l; simpl; intros. contr. destruct H0. subst a. apply in_appl. exact H. ded (IHl H H0). apply in_appr. exact H1. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)