proposition: Lemma incl_svars l1 l2 : incl l1 l2 -> incl (svars l1) (svars l2).
proof: Proof. intros. unfold incl. intros. ded (in_svars_elim H0). do 2 destruct H1. eapply in_svars_intro. apply H2. apply H. exact H1. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)