proposition: Lemma ob_discrete_cat : forall z x, ob (discrete_cat z) x = inc x z.
proof: Proof. ir. ap iff_eq; ir. ufi discrete_cat H. rwi ob_subcategory H. ee. rwi ob_function_cat H. am. ap discrete_cat_property. uf discrete_cat. rw ob_subcategory. ee; try tv. rww ob_function_cat. ap discrete_cat_property. Qed.
imports: Arith ordinal nat_trans