(5steps 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: compose flips append
  k:, L1,L2:(k-1) List.
  compose_flips(L1) o compose_flips(L2) = compose_flips(L1 @ L2)
By: Auto THEN Unfold `compose_flips` 0

Generated subgoal:

1 1. k : 
2. L1 : (k-1) List
3. L2 : (k-1) List
  compose_list(map(i.(i, i+1);L1)) o compose_list(map(i.(i, i+1);L2))
  =
  compose_list(map(i.(i, i+1);L1 @ L2))
   kk
4 steps

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

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