simp only [mem_singleton_iff, insert_eq_of_mem, encard_singleton]
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e : α
⊢ {e, e}.encard ≤ 2
case inl
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
e : α
⊢ 1 ≤ 2