exact absurd hb.1 hl.head
case refl
α : 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
hpa : p a = true
hb : a ∈ l ∧ p a = true
⊢ (if p a = true then 1 else 0) ≤ 0
no goals