proposition: Lemma activeEnv_lift : forall M n, activeEnv (lift M n) [=] liftedEnv n (activeEnv M) 0.
proof: Proof. intros; unfold lift. apply activeEnv_lift_aux. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)