no goals
α : Type ?u.373790
β : Type ?u.373793
γ : Type ?u.373796
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
⊢ ∀ (i : ι), f i ≠ mex f
simpa using mex_not_mem_range.{_, v} f