proposition: Lemma activeEnv_appBodyR_varD : forall M (Mapp: isApp M), envSubset (activeEnv (appBodyR 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_ry; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)