rintro ⟨l,hyp⟩
case mp
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (∃ a ∈ allTP α, evaluate M w (Con (Xset α a φ))) → ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f
case mp.intro
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
l : TP α
hyp : l ∈ allTP α ∧ evaluate M w (Con (Xset α l φ))
⊢ ∃ a ∈ allTP α, ∀ f ∈ Xset α a φ, evaluate M w f