proposition: Lemma absBody_eq : forall M N (Mabs: isAbs M) (Nabs: isAbs N), M = N -> absBody Mabs = absBody Nabs.
proof: Proof. intros; term_inv M; term_inv N. injection H; intros. apply term_eq; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)