proposition: Lemma fob_discrete_functor : forall z a f x, discrete_functor_property z a f -> inc x z -> fob (discrete_functor z a f) x = f x.
proof: Proof. ir. uf fob. rw fmor_discrete_functor. rw source_discrete_functor. rw source_id. rw source_id. tv. rww ob_discrete_cat. rw source_id. uh H; ee. au. rww ob_discrete_cat. rw source_discrete_functor. app mor_id. rww ob_discrete_cat. Qed.
imports: Arith ordinal nat_trans