proposition: Lemma vars_shift : forall t, vars (shift t) = map shift_var (vars t).
proof: Proof. apply term_ind with (Q := fun n (v : terms n) => vars_vec (Vmap shift v) = map shift_var (vars_vec v)); intros. refl. unfold shift. rewrite sub_fun, !vars_fun. exact H. refl. simpl. rewrite map_app, H. apply appr_eq. exact H0. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)