proposition: Lemma ordinal_punctured_downward : forall o x, is_ordinal o -> inc x o -> punctured_downward_subset (obi o) x = x.
proof: Proof. ir. uf punctured_downward_subset; ap extensionality; uhg; ir. Ztac. rwi ordinal_obi_lt H3. ee; am. am. ap Z_inc. rw obi_U. ap ordinal_inc_trans. sh x. ee; am. am. rw ordinal_obi_lt. ee; am. am. Qed.
imports: Arith transfinite