1. T : Type
2. l : T List
3. x : T
4. i,j:. i<||l||  j<||l||  i = j  l[i] = l[j]
5. (x  l)
6. i : 
7. j : 
8. i<||l||+1
9. j<||l||+1
10. i = j
  [x / l][i] = [x / l][j]

By:	CaseNat 0 `i' THEN CaseNat 0 `j' THEN Reduce 0 THEN RWO Thm* a:T, as:T List, i:. 0<i  i||as||  [a / as][i] = as[(i-1)] 0 THEN Try BackThruSomeHyp THEN Try (ParallelOp 5 THEN Unfold `l_member` 0) THEN Try (InstConcl [j-1] THEN Complete Auto) THEN Try (InstConcl [i-1] THEN Complete Auto)

None

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