IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
firstn is iseg11122 1. T : Type
2. T List
3. l : T List
4. u : T 5. v : T List
6. v = firstn(||v||;v @ l)
[u / v] = [u / firstn(||v||;v @ l)]
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
[u / v] = [u / firstn(||v||;v @ l)]
