proposition: Lemma is_subcategory_property : forall a b, is_subcategory a b -> subcategory_property b (ob a) (mor a).
proof: Proof. ir. cp H. uh H; ee. uhg; ee. am. ir. wr H5. rww mor_comp. am. am. am. ir. wr (is_subcategory_same_id H0). app mor_id. am. ir. rww ob_source. ir. rww ob_target. Qed.
imports: Arith ordinal nat_trans