Theorem: LeanSAT.Model.PropFun.satisfies_impl' (LeanSAT/Model/PropFun.lean)

State before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ φ₁ ⇨ φ₂ ↔ (fun M φ => ¬M ⊨ φ) τ φ₁ ∨ τ ⊨ φ₂
Tactic:
simp only [sEntails, satisfies, eval_impl, HImp.himp]
State after:
ν : Type u_1
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
⊢ (max (eval τ φ₂) !eval τ φ₁) = true ↔ ¬eval τ φ₁ = true ∨ eval τ φ₂ = true

State before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
⊢ (max (eval τ φ₂) !eval τ φ₁) = true ↔ ¬eval τ φ₁ = true ∨ eval τ φ₂ = true
Tactic:
cases (eval τ φ₁) <;> simp [himp_eq]
State after:
no goals