is mentioned by
Thm* y = z x = y (x, y) = compose_list([(x, z); (y, z); (x, z)]) | [flip_lemma] |
Thm* compose_list(L1) o compose_list(L2) = compose_list(L1 @ L2) | [compose_append] |
[compose_flips] |
Try larger context:
MarkB generic
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html