Nuprl - Proof: cons member 1 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: cons member 1 2 1 1

1. T : Type
2. l : T List
3. a : T
4. x : T
5. i :

6. i

0
7. 0<i
8. i<||l||+1
9. x = l[(i-1)]

x = a

(

. i<||l|| & x = l[i])

By:	Sel 2 (Analyze 0) THEN InstConcl [i-1]

Generated subgoals:

None

About:

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