mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def (f o g)(x) == f(g(x))

is mentioned by

Thm* k:, L1,L2:(k-1) List.
Thm* compose_flips(L1) o compose_flips(L2) = compose_flips(L1 @ L2)		[compose_flips_append]
Thm* L1,L2:(TT) List.
Thm* compose_list(L1) o compose_list(L2) = compose_list(L1 @ L2)		[compose_append]
Thm* f,g:(TT). Bij(T; T; f)  Bij(T; T; g)  Bij(T; T; f o g)[compose_bij]
Def compose_list(L) == reduce(p,q. p o q;x.x;L)[compose_list]

In prior sections: fun 1 list 1 mb nat mb list 1

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb list 2 Sections MarkB generic Doc