simp only [List.all_eq_true, decide_eq_true_eq]
α : 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
no goals