proposition: Lemma term_env_activeEnv : forall M, env M = env M [+] activeEnv M.
proof: Proof. intros. apply env_subset_as_sum_r. apply activeEnv_length. apply activeEnv_subset. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)