IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
for hdtl wf A,B,C:Type, f:(BCC), k:C, as:A List, g:(A(A List)B).
(ForHdTl{A,f,k} h::tas. g(h,t)) C
By:
Unfold `for_hdtl` 0 THEN RepD
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A,B,C:Type, f:(B
C
(ForHdTl{A,f,k} h::t 
as. g(h,t)) 
