no goals
α : Type ?u.306687
β : Type ?u.306690
γ : Type ?u.306693
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal
ho : type r = o
ho' : type r' = o
f : (a : Ordinal) → a < o → Ordinal
⊢ range (familyOfBFamily' r ho f) = range (familyOfBFamily' r' ho' f)
simp