proposition: Lemma var_notSubst_lift_rev G x i : (lift_subst G i) |-> x/- -> G |-> x/- .
proof: Proof. intros Gxn. destruct Gxn. left; apply nth_lift_subst_n_rev with i; trivial. right; apply nth_lift_subst_sn_rev with i; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)