proposition: Lemma var_subst_lift_rev G x i T : (lift_subst G i) |-> x/T -> exists T', G |-> x/T' /\ T = lift T' i.
proof: Proof. intros Gx_T. unfold varSubstTo. destruct (nth_lift_subst_s_rev G i x Gx_T) as [W [GW LW]]. exists W; split; try_solve. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)