proposition: Lemma abs_proof_irr : forall M (Mabs Mabs': isAbs M), Mabs = Mabs'.
proof: Proof. intro M; term_inv M. dependent inversion Mabs; dependent inversion Mabs'; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)