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

State before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ φ₁ ⇨ φ₂ ↔ τ ⊨ φ₁ → τ ⊨ φ₂
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