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

State before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ τ ⊨ impl φ₁ φ₂ ↔ (fun M φ => ¬M ⊨ φ) τ φ₁ ∨ τ ⊨ φ₂
Tactic:
simp only [sEntails, satisfies, eval]
State after:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ eval τ φ₁ ⇨ eval τ φ₂ = true ↔ ¬eval τ φ₁ = true ∨ eval τ φ₂ = true

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