The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

Right, fair enough. So the general answer is: 'leaves' is not  
constructively definable (unless we modify the codomain to include  
some sort of delay). That makes sense :) Thanks everybody for your  
answers; most helpful, as always.

Edsko