[Agda] Absurd question

[Martin Escardo]

On 23/05/13 23:37, Martin Escardo wrote:
> But, still, this requires redefining the natural formulations into
> unnatural ones. (You would have to see the file to appreciate the
> unnaturality, reported in the comments.)

Ignoring the parenthetical remark, this is odd, because once a theorem 
is proved, it is proved. It shouldn't make a difference whether its 
proof uses \() or y.

But in this case, the uses of the theorem are rejected if its proof uses 
\(), and accepted if its proof uses y.

Martin