IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
firstn is iseg111211 1. T : Type
2. T List
3. l : T List
4. u : T 5. v : T List
6. v = firstn(||v||;v @ l)
7. 0<||v||+1
[u / firstn(||v||+1-1;v @ l)] ~ [u / firstn(||v||;v @ l)]
By:
Subst' (||v||+1-1 = ||v||) 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
[u / firstn(||v||+1-1;v @ l)] ~ [u / firstn(||v||;v @ l)]
