α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ (bif p a then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 0
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ countp p (a :: l) = countp p l
change (bif _ then _ else _) = countp.go _ _ _
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ (bif false then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 0
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ (bif p a then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 0
rw [Bool.of_not_eq_true pa]
no goals
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : ¬p a = true
⊢ (bif false then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 0
rfl