rw [tautImp_iff_comboNotUnsat]
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable (θ :: X.right)
⊢ θ⊨ψ
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ¬satisfiable (θ :: X.right)
⊢ ¬satisfiable [θ, ~ψ]