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

Generated subgoals:

None

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

(9steps total) PrintForm Definitions Lemmas mb event system 2 Sections EventSystems Doc