Как импортировать `∃-синтаксис`?

open import Data.Product using (_×_; ∃; ∃-syntax)
open import Data.List

Any-∃ : ∀ {A : Set} {P : A → Set} {xs : List A} → ∃[ x ∈ xs ] P x

Could not parse the application ∃[ x ∈ xs ] P x
Operators used in the grammar:
  ∃[_] (prefix notation, level 20) [∃-syntax (C:\Users\Marko\AppData\Roaming\cabal\x86_64-windows-ghc-8.6.5\Agda-2.6.0\lib\agda-stdlib\src\Data\Product.agda:78,1-9)]
when scope checking ∃[ x ∈ xs ] P x

По какой-то причине кажется, что он неправильно импортирует приоритет из стандартного библиотечного модуля. Определив его как...

Any-∃ : ∀ {A : Set} {P : A → Set} {xs : List A} → ∃[ x ] P x

... заставит его пройти синтаксический анализ, но я не уверен, что это правильно для одной из проблем, которые я пытаюсь решить.

Что мне здесь делать?