proposition: Lemma conv_env_lower : forall M Menv, conv_env M (lower M Menv) (lowerEnvSubst 0 (length (env M))).
proof: Proof. intros. intros x y Qxy A. rewrite !activeEnv_lower. unfold loweredEnv; autorewrite with datatypes terms using simpl. destruct x; try_solve. destruct (eq_nat_dec 0 0); try_solve. destruct (eq_nat_dec 0 (S x)); try_solve. inversion Qxy. destruct (activeEnv M); try_solve. split; destruct y; try_solve. rewrite (finalSeg_cons o e); try_solve. inversion H0; try_solve. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)