The Coq mailing list

[popescu2 AT uiuc.edu]

Hello, 

Maybe it is just my ignorance about Coq speaking now, but 
working with boolean predicates P : Less n -> bool does not seem to help 
either, since then the functions f would be in 
f : {i : Less n | P i = true} -> nat and after matching P n' with true I do 
not seem to have access to a proof of 
P i = true in order to apply f to n'. 

(In this and the previous message, I have identified elements of Less n with 
elements of nat, in the "Program" style, to keep the ideas clear.)

Regards, 
   Andrei