proposition: Lemma inc_homs_target : forall a u, is_ob from_arrows a -> (exists b, (is_ob from_arrows b & inc u (homs b a))) -> target u = a.
proof: Proof. ir. nin H0. ee. rwi is_ob_from_arrows H. rwi is_ob_from_arrows H0. cp property_hyp. uh H2; ee. exact (H3 _ _ _ H1). Qed.
imports: Arith ordinal nat_trans