have ⟨σ₂, hAgree₂, hσ₂⟩ := h₁ σ₁ hσ₁
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₁ : PropAssignment ν
hAgree₁ : PropAssignment.agreeOn X σ₁ τ
hσ₁ : σ₁ ⊨ φ₁
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₁ : PropAssignment ν
hAgree₁ : PropAssignment.agreeOn X σ₁ τ
hσ₁ : σ₁ ⊨ φ₁
σ₂ : PropAssignment ν
hAgree₂ : PropAssignment.agreeOn X σ₂ σ₁
hσ₂ : σ₂ ⊨ φ₂
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂