proposition: Lemma presubst_prelift_aux : forall M G i j, presubst_aux (prelift_aux j M i) i (copy (i + j) None ++ lift_subst G j) = prelift_aux j (presubst_aux M i (copy i None ++ G)) i.
proof: Proof. induction M; simpl; intros. destruct (Compare_dec.le_gt_dec i x); simpl. rewrite !nth_app_right; autorewrite with datatypes using trivial; try lia. replace (x + j - (i + j)) with (x - i); [idtac | lia]. destruct (varSubst_dec G (x-i)) as [[W GW] | Gn]. rewrite GW. rewrite (var_subst_lift j GW). autorewrite with terms. rewrite <- prelift_fold. unfold prelift; rewrite prelift_aux_fold_aux; try_solve; try lia. rewrite Nat.add_comm; trivial. destruct (var_notSubst_lift j Gn); destruct Gn; rewrite H; rewrite H0; simpl; destruct (Compare_dec.le_gt_dec i x); solve [ lia | assert (S x = (x + 1)%nat); [lia | try_solve] ]. rewrite !nth_app_left; autorewrite with datatypes using trivial; try lia. simpl. destruct (Compare_dec.le_gt_dec i x). lia. rewrite nth_app_left; autorewrite with datatypes using trivial; try lia. trivial. replace (None :: copy (i + j) None ++ lift_subst G 1) with (copy (S i + j) None ++ lift_subst G 1); trivial. rewrite <- (IHM G (S i)); trivial. rewrite <- IHM1. rewrite <- IHM2. trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)