simp only [sEntails, satisfies, eval_impl, eval_disj, eval_neg]
case a
ν : Type u_1
φ ψ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ impl φ ψ ↔ τ ⊨ disj ψ (neg φ)
case a
ν : Type u_1
φ ψ : PropFun ν
τ : PropAssignment ν
⊢ eval τ φ ⇨ eval τ ψ = true ↔ (eval τ ψ || !eval τ φ) = true