Nuprl - Proof: pairwise-cons 2 1 1 1

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

1. T : Type
2. x : T
3. L : T List
4. P : T

Prop
5.

||[x / L]||, j:

i. P([x / L][j],[x / L][i])
6. y : T
7. i :

8. i<||L||
9. y = L[i]
10. P(x,L[i])

P(x,y)

By:	RevHypSubst -2 -1

Generated subgoals:

None

About:

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