Theorem: List.countp_nil (One.lean)

State before:
α✝ : Type u_1
p : α✝ → Bool
⊢ countp p [] = 0
Tactic:
unfold countp countp.go
State after:
α✝ : Type u_1
p : α✝ → Bool
⊢ 0 = 0

State before:
α✝ : Type u_1
p : α✝ → Bool
⊢ 0 = 0
Tactic:
rfl
State after:
no goals