proposition: Lemma absBody_type : forall M (Mabs: isAbs M) A B, type M = A --> B -> type (absBody Mabs) = B.
proof: Proof. intros M Mabs A B MAB. term_inv M; congruence. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)