IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
It is a bad idea to make these usual wf lemmas since often one mixes integer funs and nat funs.
(e.g. n:, i:{0...n}. -i+n)
Sometime maybe should figure out systematic way of dealing with , polymorphism
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
n:
, i:{0...n}. -i+n 
polymorphism
