proposition: Lemma envMinimal_app : forall M Ml Mr (Mapp: isApp M), envMinimal Ml -> envMinimal Mr -> env Ml [<->] env Mr -> env M = env Ml [+] env Mr -> term M = term Ml @@ term Mr -> envMinimal M.
proof: Proof. unfold envMinimal; intros. rewrite activeEnv_app with M Mapp. rewrite H2. rewrite (@activeEnv_minimal (appBodyL Mapp) Ml); trivial. rewrite (@activeEnv_minimal (appBodyR Mapp) Mr); trivial. rewrite H; rewrite H0; trivial. rewrite appBodyR_env. rewrite H2. apply env_comp_ext_l. rewrite (appBodyR_term M H3); trivial. rewrite appBodyL_env. rewrite H2. apply env_comp_sym. apply env_comp_sum; auto with terms. rewrite (appBodyL_term M H3); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)