if hpa : p a = true then
  have : a = b := hp _ _ hpa hb.2
  cases this
  exact absurd hb.1 hl.head
else
  rewrite [if_neg hpa]; exact .refl
case cons.inl.a
α : Type u
β : Type v
p : α → Bool
hp : ∀ (a b : α), p a = true → p b = true → a = b
a : α
l : List α
IH : Nodup l → countP p l ≤ 1
hl : Nodup (a :: l)
hone : countP p l = 1
b : α
hb : b ∈ l ∧ p b = true
⊢ (if p a = true then 1 else 0) ≤ 0
no goals