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