aesop
W✝ : Type
M : KripkeModel W✝
w : W✝
⊢ ∀ (p : List Formula × List Program → Formula) (X : List (List Formula × List Program)),
    (∃ f ∈ List.map p X, evaluate M w f) ↔ ∃ Fδ ∈ X, evaluate M w (p Fδ)
no goals