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