proposition: Lemma lower_env : forall M ME, env (lower M ME) = loweredEnv (env M) 0.
proof: Proof. intros; unfold lower. destruct (lower_aux M ME); try_solve. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)