intro W M w
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), evaluate x_1 x_2 θ → evaluate x_1 x_2 ψ
⊢ ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), evaluate x_1 x_2 θ → evaluate x_1 x_2 ψ
case h.right.right
φ ψ : Formula
hyp : φ⊨ψ
X : TNode := ([φ], [~ψ], none)
ctX : ClosedTableau ([], []) X
θ : Formula
this : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), evaluate x_1 x_2 θ → evaluate x_1 x_2 ψ
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w θ → evaluate M w ψ