proposition: Lemma activeEnv_app_comp : forall M (Mapp: isApp M), activeEnv (appBodyL Mapp) [<->] activeEnv (appBodyR Mapp).
proof: Proof. intros M Mapp p A B LA RB. set (l := activeEnv_subset (appBodyL Mapp) LA). rewrite appBodyL_env in l. set (r := activeEnv_subset (appBodyR Mapp) RB). rewrite appBodyR_env in r. inversion l; inversion r; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)