cases hpa : p a <;> simp only [if_pos, if_neg, Nat.add_zero]
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
⊢ (countP p l + if p a = true then 1 else 0) ≤ countP p l'
case cons.false
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = false
⊢ countP p l ≤ countP p l'

case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
⊢ countP p l + 1 ≤ countP p l'