(4steps total) PrintForm Definitions mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: compose append
  T:Type, L1,L2:(TT) List.
  compose_list(L1) o compose_list(L2) = compose_list(L1 @ L2)
By: InductionOnList THEN Unfold `compose_list` 0 THEN Reduce 0
THEN
Fold `compose_list` 0

Generated subgoals:

1 1. T : Type
2. (TT) List
3. L2 : (TT) List
  (x.x) o compose_list(L2) = compose_list(L2)
1 step
2 1. T : Type
2. (TT) List
3. u : TT
4. v : (TT) List
5. L2:(TT) List. compose_list(v) o compose_list(L2) = compose_list(v @ L2)
6. L2 : (TT) List
  u o compose_list(v) o compose_list(L2) = u o compose_list(v @ L2)
2 steps

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

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