simp [consistent,inconsistent] at hyp
φ ψ : Formula
hyp : ¬consistent ([φ], [~ψ], none)
X : TNode := ([φ], [~ψ], none)
⊢ ClosedTableau ([], []) X
φ ψ : Formula
X : TNode := ([φ], [~ψ], none)
hyp : Nonempty (ClosedTableau LoadHistory.nil ([φ], [~ψ], none))
⊢ ClosedTableau ([], []) X