IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
compose iter prod21 1. A : Type
2. x : A 3. f : AA 4. i : 5. j : 6. k:. k = ijf{i}{j}(x) = f{k}(x)
f{i}{j}(x) = f{ij}(x)
By:
BackThru: Hyp:-1 ...
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A
k:
j 
f{
i}{
f{
