proposition: Lemma mor_discrete_cat3 : forall z u, mor (discrete_cat z) u = (inc (source u) z & inc (target u) z & source u = target u & is_id_fun_arrow u & u = id (discrete_cat z) (source u) & u = id (function_cat z) (source u)).
proof: Proof. ir. rw mor_discrete_cat; ap iff_eq; ir; xd. uh H0. rw H0. rw target_fa_id. am. uh H0. rw H0. rw source_fa_id. rww target_fa_id. rw id_discrete_cat. rw id_function_cat. am. am. am. rw id_function_cat. am. am. Qed.
imports: Arith ordinal nat_trans