proposition: Lemma sow_exists : forall p, exists o, is_sow p o.
proof: Proof. ir. apply by_cases with (exists x, is_ordinal x & p x). ir. sh (choose (is_smallest_ordinal_with p)). cp (exists_smallest_ordinal_with H). cp (choose_pr H0). cbv beta in H1. uhg; ee. uh H1; ee. am. ir. am. ir. sh emptyset. uhg; ee. ap emptyset_ordinal. ir. elim (H H0). Qed.
imports: Arith transfinite