theorem Set.ncard_singleton_inter' {α : Type u_1} (a : α) (s : Set α) [Decidable (a ∈ s)] : ({a} ∩ s).ncard = if a ∈ s then 1 else 0

theorem Set.ncard_inter_singleton {α : Type u_1} (a : α) (s : Set α) [Decidable (a ∈ s)] : (s ∩ {a}).ncard = if a ∈ s then 1 else 0