proposition: Lemma discrete_functor_property_fob : forall z a g, Functor.axioms g -> source g = discrete_cat z -> a = target g -> discrete_functor_property z a (fob g).
proof: Proof. ir. uhg; ee. uh H; ee. rww H1. ir. rw H1. ap ob_fob. am. rw H0. rw ob_discrete_cat. am. Qed.
imports: Arith ordinal nat_trans