no goals
s : Set Ordinal
a : Ordinal
⊢ (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a) ↔
    ∃ o _ho f, (∀ (i : Ordinal) (hi : i < o), f i hi ∈ s) ∧ bsup o f = a
simp only [exists_prop]