proposition: Lemma activeEnv_minimal_aux : forall M M', env M [<->] env M' -> term M = term M' -> envSubset (activeEnv M) (activeEnv M').
proof: Proof. destruct M as [E Pt T M]; induction M; intros; term_inv M'. inversion H0. apply env_subset_single. rewrite (H x A A0); trivial. unfold VarD, decl, EmptyEnv; apply nth_after_copy. rewrite H2; trivial. fold (activeEnv (buildT M)); fold (activeEnv (buildT T)); fold (activeEnv (buildT M)) in IHM. apply env_subset_tail. inversion H0. apply IHM; simpl; trivial. unfold decl; apply env_comp_cons; trivial. left; try_solve. fold (activeEnv (buildT M1)) in *; fold (activeEnv (buildT T1)). fold (activeEnv (buildT M2)) in *; fold (activeEnv (buildT T2)). inversion H0. apply env_subset_sum. change (buildT T1) with (appBodyL (M:=buildT (TApp T1 T2)) I). change (buildT T2) with (appBodyR (M:=buildT (TApp T1 T2)) I). apply activeEnv_app_comp. apply IHM1; simpl; trivial. apply IHM2; simpl; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)