proposition: Lemma activeEnv_app : forall M (Mapp: isApp M), activeEnv M = activeEnv (appBodyL Mapp) [+] activeEnv (appBodyR Mapp).
proof: Proof. intros M; term_inv M. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)