The Coq mailing list

[Benjamin Werner <benjamin.werner AT polytechnique.fr>]

Hi,

>  Correspondingly, there's no way you can construct a predicate
> P on functions such that P f is inhabited and P g is empty when f and g
> agree on all arguments: the only thing P can do with its function is
> apply it.

Actually you can construct such a predicate. You will be able to 
exhibit a proof of P f. It will also be true that there is no closed 
proof of P g. However, you will not be able to prove this last 
statement inside the system; you can only convince yourself that it is 
true by using again an argument of the form "if I had a closed proof, 
then this proof would have to be of the form ... and this is not 
possible since ... and ... are not convertible".

If I am too obscure here, I can try to elaborate when I have a little 
more time.


Cheers,


Benjamin