no goals
case h.e'_2.h.e'_1
α : Type ?u.383183
β : Type ?u.383186
γ : Type ?u.383189
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
i : Ordinal
hi : i < o
⊢ i = typein (fun x x_1 => x < x_1) (enum (fun x x_1 => x < x_1) i (_ : i < type fun x x_1 => x < x_1))
rw [typein_enum]
no goals
α : Type ?u.383183
β : Type ?u.383186
γ : Type ?u.383189
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
i : Ordinal
hi : i < o
⊢ i < type fun x x_1 => x < x_1
rwa [type_lt]