Theorem: tautImp_iff_TNodeUnsat (Pdl/LocalTableau.lean)

State before:
φ ψ : Formula
X : TNode
⊢ X = ([φ], [~ψ], none) → (φ⊨ψ ↔ ¬satisfiable X)
Tactic:
intro defX
State after:
φ ψ : Formula
X : TNode
defX : X = ([φ], [~ψ], none)
⊢ φ⊨ψ ↔ ¬satisfiable X

State before:
φ ψ : Formula
X : TNode
defX : X = ([φ], [~ψ], none)
⊢ φ⊨ψ ↔ ¬satisfiable X
Tactic:
subst defX
State after:
φ ψ : Formula
⊢ φ⊨ψ ↔ ¬satisfiable ([φ], [~ψ], none)

State before:
φ ψ : Formula
⊢ φ⊨ψ ↔ ¬satisfiable ([φ], [~ψ], none)
Tactic:
simp [satisfiable,evaluate,modelCanSemImplyTNode,formCanSemImplyForm,semImpliesLists] at *
State after:
no goals