no goals
α : Type ?u.366130
β : Type ?u.366133
γ : Type ?u.366136
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
H : IsNormal f
o : Ordinal
h : IsLimit o
⊢ (Ordinal.bsup o fun x x_1 => f x) = f o
rw [← IsNormal.bsup.{u, u, v} H (fun x _ => x) h.1, bsup_id_limit h.2]