proposition: Lemma lower_subst_aux : forall M G i, env M |= i :! -> presubst_aux (prelower_aux (term M) i) i (copy i None ++ G) = prelower_aux (presubst_aux (term M) i (copy i None ++ None :: lift_subst G 1)) i.
proof: Proof. destruct M as [E Pt TM M]. induction M; intros G i Mi; unfold prelower, presubst; simpl. destruct (Compare_dec.le_gt_dec i x); simpl. destruct (eq_nat_dec i x). rewrite e in Mi. exfalso; eapply varD_UD_absurd; eauto. destruct x; simpl. lia. replace (copy i None ++ None :: lift_subst G 1) with ((None :: copy i None) ++ lift_subst G 1). simpl. repeat rewrite nth_app_right; rewrite copy_length; try lia. destruct (varSubst_dec G (x - i)) as [[T GT] | Gn]. rewrite GT, (nth_lift_subst_s G 1 (x - i) GT), !lift_term, <- prelift_fold. apply prelower_prelift. set (w := var_notSubst_lift 1 Gn). inversion Gn; inversion w; rewrite H; rewrite H0; simpl; destruct (Compare_dec.le_gt_dec i (S x)); solve [trivial | lia]. rewrite <- list_app_first_last. rewrite <- copy_add; trivial. rewrite <- app_nil_end; trivial. rewrite !nth_app_left, nth_copy_in. simpl. destruct (Compare_dec.le_gt_dec i x); trivial. lia. lia. rewrite copy_length; lia. rewrite copy_length; lia. trivial. set (w := IHM G (S i)). simpl in w. rewrite w; trivial. rewrite IHM1; trivial. rewrite IHM2; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)