proposition: Lemma conv_term_lifted_aux : forall M N i Q, conv_term M N Q -> (forall j, j < i -> Q.(envSub) j j) -> conv_term (prelift_aux 1 M i) (prelift_aux 1 N i) (envSubst_lift1 Q).
proof: Proof. intros M N i Q MNQ; gen i; clear i. induction MNQ; intros; simpl. destruct S. destruct (le_gt_dec i x). destruct (le_gt_dec i y). constructor; simpl. replace (x + 1) with (S x); [idtac | lia]. replace (y + 1) with (S y); [trivial | lia]. absurd (x = y). lia. apply envSub_Rok0 with y; trivial. apply H0; trivial. destruct (le_gt_dec i y). absurd (x = y). lia. apply envSub_Lok0 with x; trivial. apply H0; trivial. destruct (eq_nat_dec x y). rewrite <- e. constructor. destruct x; destruct y; simpl; trivial. apply H0; lia. apply H0; lia. absurd (x = y); trivial. apply envSub_Lok0 with x; trivial. apply H0; trivial. constructor 2. constructor 3. apply IHMNQ. intros j ji. destruct j. destruct S; try_solve. destruct S. simpl; apply H; lia. constructor 4. apply IHMNQ1; trivial. apply IHMNQ2; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)