#### Exercise `Any-∃`
Show that `Any P xs` is isomorphic to `∃[ x ∈ xs ] P x`.
Оставляя в стороне тот факт, что ∃[ x ∈ xs ] P x даже не допустимый синтаксис - только Σ[ x ∈ xs ] P x может быть допустимым, ни одна из сигнатур типов, которые я пробовал проверять на наличие ошибок для этой конкретной проблемы.
Any-∃ : ∀ {A : Set} {P : A → Set} {xs : List A} → Any P xs ≃ Σ[ x ∈ xs ] P x
List A !=< Set _a_1582 of type Set
when checking that the expression xs has type Set _a_1582
Самая очевидная вещь здесь терпит неудачу. Я вроде понимаю, что вопрос пытается задать мне здесь, но я не уверен, какой должна быть структура ∃[ x ∈ xs ] P x.
Это предпоследнее упражнение в главе Списки книги PLFA.