proposition: Lemma shift_terms_correct : forall l p, pw_disjoint_vars (shift_terms p l).
proof: Proof. induction l. unfold pw_disjoint_vars. intros. contr. intro. simpl. apply pw_disjoint_vars_cons. apply IHl. unfold disjoint_vars. intros. ded (in_vars_shift_max H0). ded (in_vars_shift_terms_min H H1). absurd (x <= maxvar a + p); lia. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)