simp [SemanticEntails.entails, satisfies, eval_of_agreeOn_vars h]
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
⊢ σ₁ ⊨ φ ↔ σ₂ ⊨ φ
no goals