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

State before:
ν : Type u_1
φ ψ : PropFun ν
⊢ impl φ ψ = disj ψ (neg φ)
Tactic:
ext τ
State after:
case a
ν : Type u_1
φ ψ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ impl φ ψ ↔ τ ⊨ disj ψ (neg φ)

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

State before:
case a
ν : Type u_1
φ ψ : PropFun ν
τ : PropAssignment ν
⊢ eval τ φ ⇨ eval τ ψ = true ↔ (eval τ ψ || !eval τ φ) = true
Tactic:
rfl
State after:
no goals