simplify a proof
prove that existence of a terminal object in a category is a proposition

  Lemma isaprop_TerminalObject (C:category) : isaprop (TerminalObject C).