proposition: Lemma subst_lift_subst Pt G i : presubst_aux Pt i G = presubst Pt (lift_subst G i).
proof: Proof. replace i with (0 + i). rewrite (subst_lift_subst_aux Pt G 0 i). unfold presubst; trivial. auto. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)