proposition: Lemma inc_V_arrow2 : forall u a x, inc u (function_arrow_set (source u) (target u)) -> inc x (source u) -> a = target u -> inc (V x (arrow u)) a.
proof: Proof. ir. ap map_V_inc. sh (source u). ee; try am. rwi inc_function_arrow_set H. rw H1; ee; am. Qed.
imports: Arith ordinal nat_trans