Theorem: helper (Pdl/Unfold.lean)

State before:
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δ)
Tactic:
aesop
State after:
no goals