no goals
α : Type u_1
β : Type ?u.97279
γ : Type ?u.97282
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : Ordinal
h₁ : o₁ < type r
h₂ : o₂ < type r
⊢ r (enum r o₁ h₁) (enum r o₂ h₂) ↔ o₁ < o₂
rw [← typein_lt_typein r, typein_enum, typein_enum]