proposition: Lemma id_inclusion_cat : forall z x, inc x z -> id (inclusion_cat z) x = fa_id x.
proof: Proof. ir. uf inclusion_cat. rw id_subcategory. rww id_function_cat. ap inclusion_cat_property. rww ob_function_cat. tv. Qed.
imports: Arith ordinal nat_trans