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