simp
case a
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) ↔ τ ⊨ PropFun.map f (toPropFun l)
no goals