http://www.icsi.berkeley.edu/pubs/techreports/tr-89-64

We check whether Alice has a correct constructive proof for
theorems of the form:

EA prop
EAEA ... prop

If Bob can choose objects for the A quantifiers so that !prop
holds, then clearly Alice' proof is not a correct constructive proof.
Her algorithm is wrong. 

It is a proof counterexample, not a counter example to the 
theorem.
Well, it shows an error in a constructive proof.

We check Alice' program only for the given predicate defining F:

E f in F

If 
======================