(31steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: permute by flips 1
1. p : 00
2. Bij(0; 0; p)
  L:(0-1) List. p = compose_flips(L)
By: InstConcl [nil] THEN Unfold `compose_flips` 0 THEN Reduce 0

Generated subgoal:

1   p = (x.x)
1 step

About:
listnilnatural_numbersubtractlambdafunctionequalexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(31steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc