Theorem: tableauThenNotSat (Pdl/Soundness.lean)

State before:
⊢ ∀ (X : TNode), ClosedTableau LoadHistory.nil X → ¬satisfiable X
Tactic:
intro X t
State after:
X : TNode
t : ClosedTableau LoadHistory.nil X
⊢ ¬satisfiable X

State before:
X : TNode
t : ClosedTableau LoadHistory.nil X
⊢ ¬satisfiable X
Tactic:
sorry
State after:
no goals