have ⟨σ₃, hA', hS'⟩ := (e σ₁).mp ⟨σ₁, σ₁.agreeOn_refl _, hS⟩
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
e : equivalentOver Y φ₁ φ₂
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₁
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
e : equivalentOver Y φ₁ φ₂
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₁
σ₃ : PropAssignment ν
hA' : PropAssignment.agreeOn Y σ₃ σ₁
hS' : σ₃ ⊨ φ₂
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂