no goals
α : Type u
β : Type v
γ : Type ?u.39622
δ : Type ?u.39625
p : α → Prop
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : OrderTop (Subtype p)
htop : p ⊤
x : { x // p x }
⊢ ↑x = ⊤ ↔ x = ⊤
rw [← coe_top htop, ext_iff]