1. A : Type
2. P : AAProp
3. X : A List
4. Y : A List
5. a : A
6. b : A
7. P(a,b)
8. i : 
9. i<||X @ [b; a / Y]||
10. i<||X||
11. i = ||X||
12. i = ||X||+1
  [b; a / Y][(i-||X||)] = [a; b / Y][(i-||X||)]

By:	RepeatFor 2 (RWO Thm* a:T, as:T List, i:. 0<i  i||as||  [a / as][i] = as[(i-1)] 0)

None

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