⊢ (type fun x x_1 => x < x_1) = type fun x x_1 => x < x_1
⊢ (type fun x x_1 => x < x_1) = Ordinal.univ
rw [Ordinal.univ_id]
no goals
⊢ (type fun x x_1 => x < x_1) = type fun x x_1 => x < x_1
exact Quotient.sound ⟨alephIdx.relIso⟩