proposition: Lemma presubst_aux_disjoint : forall Pt Pt_x G i k (shift := fun k G => copy k None ++ G) (EL := shift k (lift_subst (None::G) (S k))) (ER := shift k {x/Pt_x}) (EC := shift k (Some Pt_x :: lift_subst G (S k))), presubst_aux (presubst_aux Pt i EL) i ER = presubst_aux Pt i EC.
proof: Proof. induction Pt; intros. unfold EL, ER, EC, shift; simpl. destruct (gt_eq_gt_dec k x) as [[x_gt_k | x_eq_k] | k_eq_x]. do 2 (rewrite nth_app_right; autorewrite with datatypes using auto with arith). assert (w_xk: exists w, x - k = S w). assert (x_k_0: x - k > 0). lia. destruct (x - k). absurd (0 > 0); auto with arith. exists n; trivial. destruct w_xk as [w w_eq]. rewrite w_eq; simpl. destruct (nth_error_In (lift_subst G (S k)) w) as [[ps ps_nth] | pn]. rewrite ps_nth. destruct ps. destruct (in_lift_subst t G (S k)) as [q q_in q_lift]. eapply nth_some_in; eauto. rewrite q_lift. rewrite <- lift_fold. unfold lift. destruct (lift_aux ((S k)+i) q 0) as [Q [Q_env [Q_term Q_type]]]; simpl. rewrite Q_term. rewrite subst_lift_subst. rewrite lift_subst_distr. rewrite lift_empty_subst. rewrite presubst_lift_beyond; trivial. lia. rewrite length_lift_subst; simpl. lia. rewrite presubst_var_beyond; trivial. autorewrite with datatypes using simpl. lia. rewrite pn. rewrite presubst_var_beyond; trivial. autorewrite with datatypes using simpl. lia. rewrite x_eq_k. do 2 (rewrite nth_app_right; autorewrite with datatypes using auto). rewrite Nat.sub_diag; simpl. rewrite nth_app_right; autorewrite with datatypes using auto. rewrite Nat.sub_diag; trivial. do 2 (rewrite nth_app_left; autorewrite with datatypes using trivial). simpl. rewrite nth_app_left; autorewrite with datatypes using trivial. auto. unfold EL, ER, EC, shift; simpl. replace (S i) with (i + 1); [idtac | lia]. rewrite !subst_lift_subst_aux; simpl. rewrite !lift_subst_distr; simpl. rewrite <- lift_subst_fold. rewrite lift_empty_subst, !app_comm_cons, copy_cons. replace (S k + 1) with (S (S k)); [idtac | lia]. rewrite <- (IHPt (lift Pt_x 1) G i (S k)); auto. simpl; trivial. simpl. unfold EL, ER, EC, shift. rewrite (IHPt1 Pt_x G i k). rewrite (IHPt2 Pt_x G i k). trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)