(3steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hd l interval 2
1. T : Type
2. l : T List
3. i : ||l||
4. j : i
  l_interval(l;j;i)[0] = l[j]
By: RWO
Thm* l:T List, i:||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)]
0

Generated subgoals:

None

About:
listnatural_numberaddsubtractuniverseequalall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(3steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc