Theorem: LeanSAT.Encode.satisfies_cardPred (LeanSAT/Encode/Card.lean)

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

State before:
ν : Type u_1
lits : Multiset (Literal ν)
P : ℕ → Prop
inst✝ : DecidablePred P
τ : PropAssignment ν
⊢ P (card lits τ) ↔ P (card lits τ)
Tactic:
simp
State after:
no goals