obtain (rfl | hne) := eq_or_ne e f
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e f : α
⊢ {e, f}.encard ≤ 2
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e : α
⊢ {e, e}.encard ≤ 2

case inr
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e f : α
hne : e ≠ f
⊢ {e, f}.encard ≤ 2