no goals
α : Type u
β : Type v
γ : Type ?u.39229
δ : Type ?u.39232
p : α → Prop
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : OrderBot (Subtype p)
hbot : p ⊥
x : { x // p x }
⊢ ↑x = ⊥ ↔ x = ⊥
rw [← coe_bot hbot, ext_iff]