proposition: Lemma in_vars_shift_terms : forall t l p, In t (shift_terms p l) -> exists u, exists q, In u l /\ t = shift q u /\ p <= q.
proof: Proof. induction l; simpl; intros. contr. destruct H. exists a. exists p. auto. ded (IHl _ H). do 3 destruct H0. destruct H1. subst t. exists x. exists x0. intuition. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)