α : Type ?u.99408
β : Type ?u.99411
γ : Type ?u.99414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
⊢ o < succ o
α : Type ?u.99408
β : Type ?u.99411
γ : Type ?u.99414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
⊢ o < type fun x x_1 => x < x_1
rw [type_lt]
no goals
α : Type ?u.99408
β : Type ?u.99411
γ : Type ?u.99414
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
⊢ o < succ o
exact lt_succ o