proposition: Lemma inc_V_arrow : forall u a x, (exists z, mor (function_cat z) u) -> inc x (source u) -> a = target u -> inc (V x (arrow u)) a.
proof: Proof. ir. nin H. rwi mor_function_cat3 H; ee. ap map_V_inc. sh (source u). ee; try am. rww H1. Qed.
imports: Arith ordinal nat_trans