intro φ₁ φ₂ τ e ⟨σ₁, hA, hS⟩
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
⊢ ∀ (φ₁ φ₂ : PropFun ν) (τ : PropAssignment ν),
    equivalentOver Y φ₁ φ₂ →
      (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) → ∃ σ₂, 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.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂