Введение в coq?

Я пытаюсь (классическим) доказать

~ (forall t : U, phi) -> exists t: U, ~phi

в Coq. Я пытаюсь доказать это противоположным образом:

1. Assume there is no such t (so ~(exists t: U, ~phi))

2. Choose arbitrary t0:U

3. If ~phi[t/t0], then contradiction with (1)

4. Therefore, phi[t/t0]

5. Conclude (forall t:U, phi)

Моя проблема связана со строками (2) и (5). Я могу' чтобы выбрать произвольный элемент из U, докажите что-нибудь о

Любые предложения (я не собираюсь использовать контрапозитив)?