no goals
α : Type ?u.349286
β : Type ?u.349289
γ : Type ?u.349292
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal
⊢ blsub (type r) (bfamilyOfFamily' r f) = blsub (type r') (bfamilyOfFamily' r' f)
rw [blsub_eq_lsub', blsub_eq_lsub']