constructor
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ (M, v)⊨(~⌈⌈δ⌉⌉ξ) ↔ Nonempty (witness M v δ ξ)
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ (M, v)⊨(~⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)

case mpr
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ Nonempty (witness M v δ ξ) → (M, v)⊨(~⌈⌈δ⌉⌉ξ)