proposition: Lemma activeEnv_abs0 : forall M (Mabs: isAbs M) A, activeEnv (absBody Mabs) |= 0 := A -> A = absType Mabs.
proof: Proof. intros. term_inv M. fold (activeEnv (buildT T)) in H. set (w := activeEnv_subset (buildT T) H). inversion w; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)