IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
cons member11 1. T : Type
2. l : T List
3. a : T 4. x : T 5. i : 6. i = 0
0<||[a / l]|| x = [a / l][0] x = a (i:. i<||l|| & x = l[i])
By:
Reduce 0 THEN Sel 1 (Analyze 0)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html