no goals
α : Type u_2
β : Type ?u.271133
γ : Type ?u.271136
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u_1
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
i : ι
⊢ bfamilyOfFamily' r f (typein r i) (_ : typein r i < type r) = f i
simp only [bfamilyOfFamily', enum_typein]