Nuprl - Proof: permute list length

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: permute list length

T:Type, L:T List, f:(

||L||

||L||). ||(L o f)|| = ||L||

By:	Unfold `permute_list` 0 THEN BackThru Thm* n:, f:(nT). \|\|mklist(n;f)\|\| = n

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