IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
list accum wf T,T':Type, l:T List, y:T', f:(T'TT'). list_accum(x,a.f(x,a);y;l) T'
By:
RepeatFor 3 (Analyze 0) THEN ListInd -1 THEN RecUnfold `list_accum` 0
THEN
Reduce 0
THEN
EasyHyp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T,T':Type, l:T List, y:T', f:(T'
T
T'
