∀ {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] {o : Ordinal.{u}}
  (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < o → α) (g : α → β),
  g ∘ Ordinal.familyOfBFamily' r ho f = Ordinal.familyOfBFamily' r ho fun i hi => g (f i hi)