simp only [List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool]
α : 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
no goals