proposition: Lemma id_discrete_cat : forall z x, inc x z -> id (discrete_cat z) x = id (function_cat z) x.
proof: Proof. ir. cp H. wri ob_discrete_cat H. uf discrete_cat. rw id_subcategory. tv. ap discrete_cat_property. rww ob_function_cat. tv. Qed.
imports: Arith ordinal nat_trans