(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
  T:Type, l:T List, i:||l||, j:i. hd(l_interval(l;j;i)) = l[j]
By: UnivCD THEN Subst (hd(l_interval(l;j;i)) ~ l_interval(l;j;i)[0]) 0

Generated subgoals:

1 1. T : Type
2. l : T List
3. i : ||l||
4. j : i
  hd(l_interval(l;j;i)) ~ l_interval(l;j;i)[0]
1 step
2 1. T : Type
2. l : T List
3. i : ||l||
4. j : i
  l_interval(l;j;i)[0] = l[j]
1 step

About:
listnatural_numberuniverseequalsqequalall
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