no goals
α : Type ?u.308792
β : Type ?u.308795
γ : Type ?u.308798
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal
⊢ bsup (type r) (bfamilyOfFamily' r f) = bsup (type r') (bfamilyOfFamily' r' f)
rw [bsup_eq_sup', bsup_eq_sup']