induction l with
| nil => exact .step .refl
| cons a l IH =>
  simp only [countP_cons]
  cases Nat.eq_or_lt_of_le (IH hl.tail) with
  | inl hone =>
    have ⟨b,hb⟩:= (countP_pos p).mp (trans Nat.zero_lt_one hone.symm)
    rewrite [hone, Nat.add_comm]
    apply Nat.succ_le_succ
    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
  | inr hlt =>
    have := Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ hlt)
    rewrite [this, Nat.zero_add]
    cases p a <;> decide
α : Type u
β : Type v
p : α → Bool
l : List α
hp : ∀ (a b : α), p a = true → p b = true → a = b
hl : Nodup l
⊢ countP p l ≤ 1
no goals