IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
factorial tail via iter null1 1. m : 2. k : 3. m = 0
(i:{k-m..k}. i+1) = 1
By:
BackThru:
Thm*f:(AAA), u:A, a,b:, e:({a..b}A).
Thm* ba (Iter(f;u) i:{a..b}. e(i)) = u ...
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
(
i:{k-m..k
}. i+1) = 1 
f:(A
A
, e:({a..b
a 
(Iter(f;u) i:{a..b
