proposition: Lemma terms_conv_conv_lift : forall M N Q, M ~(Q) N -> (lift M 1) ~(envSubst_lift1 Q) (lift N 1).
proof: Proof. intros; constructor. rewrite !lift_term. apply conv_term_lifted. destruct H; trivial. apply conv_env_lifted; destruct H; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)