Próbuję (klasycznie) udowodnićWstępne wprowadzenie w coq?
~ (forall t : U, phi) -> exists t: U, ~phi
w Coq. Próbuję to udowodnić w sposób przeciwny:
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)
Mój problem dotyczy linii (2) i (5). Nie mogę się dowiedzieć, jak wybrać dowolny element U, dowieść czegoś o tym, że jest on , i zawrzeć forall.
Jakieś sugestie (nie jestem zobowiązana do używania contrapositive)?