no goals
α : Type ?u.352278
β : Type ?u.352281
γ : Type ?u.352284
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
a : Ordinal
⊢ a < blsub o f ↔ ∃ i hi, a ≤ f i hi
simpa only [not_forall, not_lt, not_le] using not_congr (@blsub_le_iff.{_, v} _ f a)