IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
count pairs wf11 1. T : Type
2. L : T List
3. P : TT 4. i : ||L||
5. j : ||L||
0if (i<j)P(L[i],L[j]) 1 else 0 fi
By:
GenConcl (((i<j)P(L[i],L[j])) = b) THEN SplitOnConclITE
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T
||L||
0
if (i<
j)
1 else 0 fi
