proposition: Lemma subst_lift_subst_aux: forall Pt G m n, presubst_aux Pt (m + n) G = presubst_aux Pt m (lift_subst G n).
proof: Proof. induction Pt. intros G m n. unfold presubst_aux. destruct (varSubst_dec G x) as [[T GxT] | Gxn]. rewrite GxT. rewrite (nth_lift_subst_s G n x GxT). rewrite Nat.add_comm. rewrite lift_fold; trivial. destruct (var_notSubst_lift n Gxn) as [Nglx | Nglx]; destruct Gxn as [Ngx | Ngx]; rewrite Ngx; rewrite Nglx; trivial. simpl; trivial. intros G m n; simpl. assert (Splus: forall m n, S (m + n) = S m + n). intros; auto with arith. rewrite Splus. rewrite (IHPt (None::G) (S m) n). simpl; trivial. intros G m n; simpl. rewrite (IHPt1 G m n). rewrite (IHPt2 G m n). trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)