constructor
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (⌈γ⌉ψ) ↔ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))
case mp
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (⌈γ⌉ψ) → evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ)))

case mpr
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis (List.map (fun ℓ => Con (Xset γ ℓ ψ)) (allTP γ))) → evaluate M w (⌈γ⌉ψ)