rw [encard_le_one_iff, Set.Subsingleton]
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ s.encard ≤ 1 ↔ s.Subsingleton
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y