Theorem: LRAT.Formula.sat_iff_forall (LeanSAT/LRAT/CNF.lean)

State before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
p : α → Bool
f : σ
⊢ ((toList f).all fun c => decide (((Clause.toList c).any fun l => decide (p l.fst = l.snd)) = true)) = true ↔
    ∀ (c : β), c ∈ toList f → ((Clause.toList c).any fun l => decide (p l.fst = l.snd)) = true
Tactic:
simp only [List.all_eq_true, decide_eq_true_eq]
State after:
no goals