proposition: Lemma activeEnv_minimal : forall M M', env M [<->] env M' -> term M = term M' -> activeEnv M = activeEnv M'.
proof: Proof. intros. apply env_equiv_eq. split. apply activeEnv_minimal_aux; trivial. apply activeEnv_minimal_aux; auto. apply env_comp_sym; trivial. apply activeEnv_minimal_len; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)