no goals
α : Type u_1
β : Type ?u.43617
γ : Type ?u.43620
δ : Type ?u.43623
ι : Sort ?u.43626
κ : ι → Sort ?u.43631
inst✝ : Preorder α
s : NonemptyInterval α
a : α
⊢ ↑s = Interval.pure a ↔ s = pure a
rw [← Interval.coe_inj, coe_pure_interval]