proposition: Lemma terms_lift_conv : forall M n, terms_conv M (lift M n).
proof: Proof. intros M n. exists (liftEnvSubst n 0 (length (env M))); constructor; simpl. rewrite lift_term. unfold prelift; apply conv_term_lift. apply conv_env_lift. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)