proposition: Lemma var_notSubst_lift G x i : G |-> x/- -> (lift_subst G i) |-> x/-.
proof: Proof. destruct 1. left; apply (nth_lift_subst_n G i x H). right; apply (nth_lift_subst_sn G i x H). Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)