simp [*, PropAssignment.map, Function.comp]
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ (∃ σ_1, σ_1 ⊨ φ ∧ PropAssignment.map g σ = PropAssignment.map g σ_1) ∧
    PropAssignment.map (g ∘ f) σ = PropAssignment.map f (PropAssignment.map g σ)
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ ∃ σ_1, σ_1 ⊨ φ ∧ (fun x => σ (g x)) = fun x => σ_1 (g x)