rw [tautImp_iff_TNodeUnsat rfl] at hyp
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
⊢ ClosedTableau ([], []) X
φ ψ : Formula
hyp : ¬satisfiable ([φ], [~ψ], none)
X : TNode := ([φ], [~ψ], none)
⊢ ClosedTableau ([], []) X