proposition: Lemma all_arrow_one_at : forall z u, mor (function_cat z) u -> source u = (R 1) -> (exists x, (inc x (target u) & u = arrow_one_at x (target u))).
proof: Proof. ir. assert (inc (V (R 0) (arrow u)) (target u)). ap inc_V_arrow. sh z; am. rw H0. ap inc_zero_one. tv. assert (inc (R 1) z). wr H0. wr ob_function_cat. rww ob_source. assert (inc (target u) z). wr ob_function_cat. rww ob_target. sh (V (R 0) (arrow u)). ee. am. ap mor_fc_extensionality. sh z; ee. am. ap mor_arrow_one_at. am. am. am. rww source_arrow_one_at. rww target_arrow_one_at. ir. rw V_arrow_arrow_one_at. rwi H0 H4. rwi inc_one H4. rww H4. ap inc_V_arrow. sh z; am. rw H0. ap inc_zero_one. tv. wrr H0. Qed.
imports: Arith ordinal nat_trans