use 0
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ ∃ i, x ∈ sbAux f g i
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
g : β → α
x : α
hx : x ∉ g '' univ
⊢ x ∈ sbAux f g 0