proposition: Lemma ob_existence_rw : forall a x, ob a x = (exists f, (mor a f & source f = x)).
proof: Proof. ir. ap iff_eq; ir. rwi ob_facts_rw H. uh H; ee. sh (id a x); xd. nin H. ee. rwi mor_facts_rw H. uh H; ee. wr H0; am. Qed.
imports: Arith universe