tauto
case h.right.left
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
W : Type
M : KripkeModel W
w : W
this : ¬evaluate M w θ → ¬evaluate M w φ
⊢ evaluate M w φ → evaluate M w θ
no goals