Nuprl - Proof: swap adjacent instance 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: swap adjacent instance 1

1. A : Type
2. P : A

Prop
3. X : A List
4. Y : A List
5. a : A
6. b : A
7. P(a,b)

P((X @ [a; b / Y])[||X||],(X @ [a; b / Y])[(||X||+1)])

By:	Subst ((X @ [a; b / Y])[\|\|X\|\|] = a) 0

Generated subgoals:

1 (X @ [a; b / Y])[||X||] = a
2 steps

2 P(a,(X @ [a; b / Y])[(||X||+1)])
3 steps

About:

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

1	(X @ [a; b / Y])[\|\|X\|\|] = a	2 steps
2	P(a,(X @ [a; b / Y])[(\|\|X\|\|+1)])	3 steps