IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
member singleton1 1. T : Type
2. a : T 3. x : T 4. i : 5. i<1
6. x = [a][i]
x = a
By:
MoveToConcl -1 THEN CaseNatZero `i' THEN Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
x = a
