proposition: Lemma activeEnv_appBodyL_varD : forall M (Mapp: isApp M), envSubset (activeEnv (appBodyL Mapp)) (activeEnv M).
proof: Proof. intro M; term_inv M. fold (activeEnv (buildT T1)); fold (activeEnv (buildT T2)); intros; intros x A0. apply env_sum_ly; trivial. apply (activeEnv_app_comp (buildT (TApp T1 T2)) I). Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)