rintro ⟨_, ⟨σ,h,rfl⟩, rfl⟩
case a.mp
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ (∃ σ, (∃ σ_1, σ_1 ⊨ φ ∧ σ = PropAssignment.map g σ_1) ∧ τ = PropAssignment.map f σ) →
    ∃ σ, σ ⊨ φ ∧ τ = PropAssignment.map (g ∘ f) σ
case a.mp.intro.intro.intro.intro
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ ∃ σ_1, σ_1 ⊨ φ ∧ PropAssignment.map f (PropAssignment.map g σ) = PropAssignment.map (g ∘ f) σ_1