unfold cardPred
ν : Type u_1
lits : Multiset (Literal ν)
P : ℕ → Prop
inst✝ : DecidablePred P
τ : PropAssignment ν
⊢ cardPred lits P τ ↔ P (card lits τ)
ν : Type u_1
lits : Multiset (Literal ν)
P : ℕ → Prop
inst✝ : DecidablePred P
τ : PropAssignment ν
⊢ P (card lits τ) ↔ P (card lits τ)