Теорема Евклида о простых числах на Agda

Прочитал недавно в книге С. Клини "Введение в метаматематику" о теореме Евклида, которая говорит, что простых чисел существует бесконечное количество. Теорема эта доказывается так же и в интуиционистской логике. Это и послужило стимулом реализовать его на Agda.

Почему вместо exist пишут forall?

А вот почему...
Читал  сегодня про экзистенциальные типы. Там автор пишет, что мол нам надо exist, а мы пишем forall, но они эквивалентны и это легко доказывается. Но доказательства автор не привел, а поскольку я сижу сейчас на интуиционистской логике и Агде, решил доказать, и поскольку доказательство ну очень простое решил, что все должны его знать.