proposition: Lemma double_subst_aux : forall M P G i (PG: correct_subst P (None :: lift_subst G 1)), presubst_aux (presubst_aux M i (copy i None ++ {x/P})) i (copy (S i) None ++ lift_subst G 1) = presubst_aux (presubst_aux M i (copy (S i) None ++ lift_subst G 1)) i (copy i None ++ {x/subst PG}).
proof: Proof. induction M; unfold presubst; intros; simpl. destruct (Compare_dec.gt_eq_gt_dec i x) as [[x_gt_i | x_eq_i] | x_lt_i]. rewrite nth_beyond; autorewrite with terms datatypes; simpl; try lia. replace (None :: copy i None ++ lift_subst G 1) with (copy (S i) None ++ lift_subst G 1); trivial. rewrite nth_app_right; autorewrite with terms datatypes; try lia. destruct (varSubst_dec G (x - S i)) as [[T GT] | Gn]. rewrite (var_subst_lift 1 GT), !lift_term, <- prelift_fold, presubst_beyond; trivial. autorewrite with datatypes using simpl; try lia. destruct (var_notSubst_lift 1 Gn); rewrite H; replace (%x) with (prelift (%0) x); trivial; rewrite presubst_beyond; solve [ trivial | autorewrite with datatypes using simpl; try lia ]. rewrite x_eq_i. rewrite nth_app_right; autorewrite with datatypes using try lia. rewrite Nat.sub_diag; simpl. replace (None :: copy x None ++ lift_subst G 1) with (copy (S x) None ++ lift_subst G 1); trivial. rewrite nth_app_left; autorewrite with datatypes terms using simpl; try lia. rewrite nth_app_right; autorewrite with datatypes terms using simpl; try lia. rewrite Nat.sub_diag; simpl. autorewrite with terms. rewrite <- presubst_prelift_comm; simpl. rewrite subst_lift_subst; simpl. rewrite lift_subst_distr. rewrite lift_empty_subst. rewrite <- copy_add; trivial. replace (None :: copy i None ++ lift_subst G 1) with (copy (S i) None ++ lift_subst G 1); trivial. rewrite !nth_app_left; autorewrite with terms datatypes using simpl; try lia. replace (None :: copy i None ++ lift_subst G 1) with (copy (S i) None ++ lift_subst G 1); trivial. replace (None :: copy i (None (A:=Term))) with (copy (S i) (None (A:=Term))); trivial. rewrite !nth_app_left; autorewrite with terms datatypes using simpl; try lia. rewrite nth_app_left; autorewrite with terms datatypes using trivial. trivial. replace (None :: copy i None ++ {x/P}) with (copy (S i) None ++ {x/P}); trivial. replace (None :: None :: copy i None ++ lift_subst G 1) with (copy (S (S i)) None ++ lift_subst G 1); trivial. replace (None :: copy i None ++ {x/subst PG}) with (copy (S i) None ++ {x/subst PG}); trivial. rewrite (IHM P G (S i) PG); trivial. replace (None :: copy i None ++ lift_subst G 1) with (copy (S i) None ++ lift_subst G 1); trivial. rewrite <- IHM1. rewrite <- IHM2. trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)