proposition: Lemma in_vars_shift_min x t : In x (vars (shift t)) -> p <= x.
proof: Proof. pattern t. apply term_ind_forall; clear t. simpl. intros. destruct H. lia. contr. intros. unfold shift in H0. rewrite sub_fun, vars_fun in H0. ded (in_vars_vec_elim H0). do 2 destruct H1. ded (Vin_map H1). do 2 destruct H3. subst x0. ded (Vforall_in H H3). auto. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)