have := localBoxTruth' γ ψ ℓ W M w
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : ∀ f ∈ Xset γ ℓ ψ, evaluate M w f
⊢ evaluate M w (⌈γ⌉ψ)
case mpr.intro.intro.intro.intro
γ : Program
ψ : Formula
W : Type
M : KripkeModel W
w : W
ℓ : TP γ
ℓ_in : ℓ ∈ allTP γ
w_φ : ∀ f ∈ Xset γ ℓ ψ, evaluate M w f
this : evaluate M w ((⌈γ⌉ψ)⋀signature γ ℓ) ↔ evaluate M w (Con (Xset γ ℓ ψ)⋀signature γ ℓ)
⊢ evaluate M w (⌈γ⌉ψ)