Nuprl - Proof: permute list select

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/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 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html