proposition: Lemma is_subcategory_extensionality : forall a b, is_subcategory a b -> is_subcategory b a -> a = b.
proof: Proof. ir. cp H. cp H0. uh H; uh H0; ee. uh H; uh H9; ee. rw H22. sy. rw H18. ap Notations.create_extensionality. ap extensionality; uhg; ir. ap ob_is_ob. ap H5. app is_ob_ob. ap ob_is_ob. ap H11. app is_ob_ob. ap extensionality; uhg; ir. ap mor_is_mor. ap H6. app is_mor_mor. ap mor_is_mor. ap H12. app is_mor_mor. ir. app H7. app is_mor_mor. app is_mor_mor. ir. app H8. app is_ob_ob. am. Qed.
imports: Arith ordinal nat_trans