proposition: Lemma abs_type_eq : forall M N (Mabs: isAbs M) (Nabs: isAbs N), absType Mabs = absType Nabs -> type (absBody Mabs) = type (absBody Nabs) -> type M = type N.
proof: Proof. intros M N Mabs Nabs absTypeEq absBodyEq. term_inv M; term_inv N; congruence. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)