simp only [sEntails, satisfies, eval]
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ τ ⊨ impl φ₁ φ₂ ↔ τ ⊨ φ₁ → τ ⊨ φ₂
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ eval τ φ₁ ⇨ eval τ φ₂ = true ↔ eval τ φ₁ = true → eval τ φ₂ = true