no goals
α : Type ?u.388606
β : Type ?u.388609
γ : Type ?u.388612
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o o' : Ordinal
f : (a : Ordinal) → a < o → Ordinal
g : (a : Ordinal) → a < o' → Ordinal
h : brange o f ⊆ brange o' g
⊢ range (familyOfBFamily o f) ⊆ range (familyOfBFamily o' g)
rwa [range_familyOfBFamily, range_familyOfBFamily]