rw [toPropFun]
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
C : Clause L
⊢ τ ⊨ toPropFun C ↔ ∃ l ∈ C, τ ⊨ LitVar.toPropFun l
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
C : Clause L
⊢ τ ⊨ any (Multiset.map LitVar.toPropFun ↑(Array.toList C)) ↔ ∃ l ∈ C, τ ⊨ LitVar.toPropFun l