proposition: Lemma is_mor_id_from_arrows : forall x, is_ob from_arrows x -> is_mor from_arrows (id from_arrows x).
proof: Proof. ir. cp H. cp property_hyp. rwi is_ob_from_arrows H0. uh H1; ee. rw is_mor_from_arrows. rww id_from_arrows. rww source_ids. rww target_ids. ee; try am. app H5. Qed.
imports: Arith ordinal nat_trans