proposition: Lemma wo_ordinal_obi_rw : forall o, is_ordinal o -> wo_ordinal (obi o) = o.
proof: Proof. ir. uf wo_ordinal. ap extensionality; uhg; ir. rwi Image.inc_rw H0. nin H0. ee. rwi wo_avatar_obi_id H1. wr H1. rwi obi_U H0. am. am. rwi obi_U H0; am. rw Image.inc_rw. sh x. ee. rw obi_U; am. ap wo_avatar_obi_id. am. am. Qed.
imports: Arith transfinite