rw [toPropFun]
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
φ : Cnf L
⊢ τ ⊨ toPropFun φ ↔ ∀ C ∈ φ, τ ⊨ Clause.toPropFun C
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
φ : Cnf L
⊢ τ ⊨ all ↑(List.map Clause.toPropFun φ.data) ↔ ∀ C ∈ φ, τ ⊨ Clause.toPropFun C