no goals
α : Type ?u.328469
β : Type ?u.328472
γ : Type ?u.328475
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
ι' : Type v
f : ι → Ordinal
g : ι' → Ordinal
h : range f ⊆ range g
⊢ range (succ ∘ f) ⊆ range (succ ∘ g)
convert Set.image_subset succ h <;> apply Set.range_comp