simp [map, toPropFun]
L : Type u
ν : Type v
inst✝⁵ : LitVar L ν
inst✝⁴ : LawfulLitVar L ν
inst✝³ : DecidableEq ν
V : Type u_1
L' : Type u_2
V' : Type u_3
inst✝² : LitVar L V
inst✝¹ : LitVar L' V'
inst✝ : LawfulLitVar L' V'
f : V → V'
l : L
τ : PropAssignment V'
⊢ τ ⊨ toPropFun (map f l) ↔ PropAssignment.map f τ ⊨ toPropFun l
L : Type u
ν : Type v
inst✝⁵ : LitVar L ν
inst✝⁴ : LawfulLitVar L ν
inst✝³ : DecidableEq ν
V : Type u_1
L' : Type u_2
V' : Type u_3
inst✝² : LitVar L V
inst✝¹ : LitVar L' V'
inst✝ : LawfulLitVar L' V'
f : V → V'
l : L
τ : PropAssignment V'
⊢ (τ ⊨ if polarity l = true then var (f (toVar l)) else (var (f (toVar l)))ᶜ) ↔
    PropAssignment.map f τ ⊨ if polarity l = true then var (toVar l) else (var (toVar l))ᶜ