proposition: Lemma terms_lower_conv : forall M (Menv: env M |= 0 :!), terms_conv M (lower M Menv).
proof: Proof. intros M Menv. exists (lowerEnvSubst 0 (length (env M))); constructor; simpl. rewrite lower_term; simpl. unfold prelower; apply conv_term_lower; trivial. apply conv_env_lower. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)