IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
compose append1 1. T : Type
2. (TT) List
3. L2 : (TT) List
(x.x) o compose_list(L2) = compose_list(L2)
By:
Ext THEN Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T) List
(
x.x) o compose_list(L2) = compose_list(L2)
