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