proposition: Lemma absBody_eq_env : forall M N (MAbs: isAbs M) (NAbs: isAbs N), env M = env N -> type M = type N -> env (absBody MAbs) = env (absBody NAbs).
proof: Proof. intros M N; term_inv M; term_inv N. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)