no goals
α : Type ?u.103999
β : Type ?u.104002
γ : Type ?u.104005
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
ho : ∀ (a : Ordinal), a < o → succ a < o
⊢ ∀ (a : Ordinal), (a < type fun a b => a < b) → succ a < type fun a b => a < b
rwa [type_lt]