constructor
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))) ↔ ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f
case mp
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))) → ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f

case mpr
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f) → ∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))