no goals
α : Type ?u.23296
β : Type ?u.23299
γ : Type ?u.23302
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
⊢ type (Quotient.out o).r = o
rw [Ordinal.type, WellOrder.eta, Quotient.out_eq]