IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
map map12 1. A : Type
2. B : Type
3. C : Type
4. f : AB 5. g : BC 6. A List
7. u : A 8. v : A List
9. map(g;map(f;v)) = map(g o f;v)
g(f(u)).map(g;map(f;v)) = g(f(u)).map(g o f;v)
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
B
g(f(u)).map(g;map(f;v)) = g(f(u)).map(g o f;v)
