Theorem: LRAT.Clause.sat_iff_exists (LeanSAT/LRAT/CNF.lean)

State before:
α : Type u_1
β : Type u_2
inst✝ : Clause α β
p : α → Bool
c : β
⊢ ((toList c).any fun l => decide (p l.fst = l.snd)) = true ↔ ∃ l, l ∈ toList c ∧ p l.fst = l.snd
Tactic:
simp only [List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool]
State after:
no goals