proposition: Lemma absBody_term : forall M (Mabs: isAbs M) A Pt, term M = \A => Pt -> term (absBody Mabs) = Pt.
proof: Proof. intro M; term_inv M; congruence. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)