use l
case mpr.intro
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ ∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))
case h
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ ∀ f ∈ Xset α l φ, evaluate M w f
⊢ l ∈ allTP α ∧ evaluate M w (Con (Xset α l φ))