case h.e'_4
α : Type ?u.272202
β : Type ?u.272205
γ : Type ?u.272208
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → α
i : Ordinal
hi : i < o
⊢ (type fun x x_1 => x < x_1) = o
α : Type ?u.272202
β : Type ?u.272205
γ : Type ?u.272208
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → α
i : Ordinal
hi : i < o
⊢ i < type fun x x_1 => x < x_1
convert hi
no goals
case h.e'_4
α : Type ?u.272202
β : Type ?u.272205
γ : Type ?u.272208
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → α
i : Ordinal
hi : i < o
⊢ (type fun x x_1 => x < x_1) = o
exact type_lt _