The Coq mailing list

[Roman Beslik <beroal AT ukr.net>]

Hi. Actually you can deconstruct a proof if it has 0 or 1 constructor. 
See http://coq.inria.fr/refman/Reference-Manual006.html#singleton "Empty 
and singleton elimination". Though I can say nothing about your 
particular problem.

On 28.04.10 17:23, Martijn Vermaat wrote:
> But unfortunately, we cannot deconstruct the proof of n<= m since it
> lives in Prop. Now, my guess is that there is no real solution to this
> problem, but then again, I'm still quite new to Coq.
>    

--
Best regards,
  Roman Beslik.