IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
permute list select T:Type, L:T List, f:(||L||||L||), i:||L||. (L o f)[i] = L[(f(i))]
By:
Auto THEN Unfold `permute_list` 0
THEN
RWO Thm*n:, f:(nT), i:n. mklist(n;f)[i] = f(i) 0
THEN
Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html