simp only [sEntails, satisfies, eval]
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ τ ⊨ biImpl φ₁ φ₂ ↔ τ ⊨ φ₁ ∧ τ ⊨ φ₂ ∨ (fun M φ => ¬M ⊨ φ) τ φ₁ ∧ (fun M φ => ¬M ⊨ φ) τ φ₂
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ decide (eval τ φ₁ = eval τ φ₂) = true ↔ eval τ φ₁ = true ∧ eval τ φ₂ = true ∨ ¬eval τ φ₁ = true ∧ ¬eval τ φ₂ = true