proposition: Lemma in_vars_shift_terms_min : forall p t l x, In t (shift_terms p l) -> In x (vars t) -> p <= x.
proof: Proof. intros. ded (in_vars_shift_terms H). do 3 destruct H1. destruct H2. subst t. ded (in_vars_shift_min H0). lia. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)