Nuprl - Proof: pairwise-cons 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: pairwise-cons 2 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])

(

L.P(x,y))

By:	Unfold `l_all` 0 THEN Unfold `l_member` -1 THEN ExRepD

Generated subgoal:

1 6. y : T
7. i :
8. i<||L||
9. y = L[i]
P(x,y)
2 steps

About:

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