proposition: Lemma var_subst_lift G x i T : G |-> x/T -> (lift_subst G i) |-> x/(lift T i).
proof: Proof. intros Gx_T. unfold varSubstTo; apply nth_lift_subst_s; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)