simp [satisfies_iff]
case mpr.intro.intro.intro.intro.a
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
l : L
hl2 : l ∈ C
hl1 : -l ∈ C
τ : PropAssignment ν
⊢ τ ⊨ toPropFun C ↔ τ ⊨ ⊤
case mpr.intro.intro.intro.intro.a
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
inst✝ : LawfulLitVar L ν
C : Clause L
l : L
hl2 : l ∈ C
hl1 : -l ∈ C
τ : PropAssignment ν
⊢ ∃ l ∈ C, τ ⊨ LitVar.toPropFun l