proposition: Lemma activeEnv_lower : forall M Menv, activeEnv (lower M Menv) = loweredEnv (activeEnv M) 0.
proof: Proof. intros. unfold lower. apply activeEnv_lower_aux. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)