∀ {α : Type u_1} [BEq α] {a : α} {b : α} {p : α → Bool} (x : α) (l : List α),
  (¬((List.countP p l + if p b = true then 1 else 0) + if p x = true then 1 else 0) =
        (List.countP p l + if p x = true then 1 else 0) + if p b = true then 1 else 0) →
    False