(26steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel exp list 1
1. T : Type
2. R : TTProp
  x,y:T.
  x = y
  
  (L:T List. 
  (||L|| = 1   & L[0] = x & last(L) = y & (i:0. L[i] R L[(i+1)]))
By: Unfold `last` 0 THEN Try (InstConcl [[x]] THEN Reduce 0) THEN ExRepD

Generated subgoal:

1 3. x : T
4. y : T
5. L : T List
6. ||L|| = 1  
7. L[0] = x
8. L[(||L||-1)] = y
9. i:0. L[i] R L[(i+1)]
  x = y
1 step

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

(26steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc