proposition: Lemma show_empty_subcategory : forall a b, Category.axioms a -> Category.axioms b -> (forall x, ob a x -> False) -> structure a = structure b -> is_subcategory a b.
proof: Proof. ir. assert (forall u, mor a u -> False). ir. apply H1 with (source u). rww ob_source. uhg; ee; try am. ir. elim (H1 _ H4). ir. elim (H3 _ H4). ir. elim (H3 _ H4). ir. elim (H1 _ H4). Qed.
imports: Arith ordinal nat_trans