simp [map, satisfies_iff]
case a
L : Type u
ν : Type v
inst✝² : LitVar L ν
L' : Type u_1
ν' : Type u_2
inst✝¹ : LitVar L' ν'
inst✝ : LawfulLitVar L' ν'
f : ν → ν'
c : Clause L
τ : PropAssignment ν'
⊢ τ ⊨ toPropFun (map L' f c) ↔ τ ⊨ PropFun.map f (toPropFun c)
no goals