subst def_φ
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
w_φ : evaluate M w φ
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
def_φ : Con (Xset γ ℓ ψ) = φ
⊢ evaluate M w (⌈γ⌉ψ)
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : evaluate M w (Con (Xset γ ℓ ψ))
⊢ evaluate M w (⌈γ⌉ψ)