proposition: Lemma conv_term_lift : forall M n k, conv_term (term M) (prelift_aux n (term M) k) (liftEnvSubst n k (length (env M))).
proof: Proof. destruct M as [E Pt T M]; induction M; unfold prelift; intros n k; simpl. destruct (le_gt_dec k x); constructor; simpl; split; try solve [ apply nth_some with (Some A); trivial | destruct (le_gt_dec k x); try solve [trivial | lia] ]. constructor 2. constructor 3. rewrite (lift_liftEnvSubst n k (length E)). apply IHM. constructor 4; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)