Nuprl - Proof: cons member 2

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

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

(

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

. i<||[a / l]|| & x = [a / l][i]

By:	Analyze -1

Generated subgoals:

1 5. x = a
i:. i<||[a / l]|| & x = [a / l][i]
1 step

2 5. i:. i<||l|| & x = l[i]
i:. i<||[a / l]|| & x = [a / l][i]
3 steps

About:

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

1	5. x = a i:. i<\|\|[a / l]\|\| & x = [a / l][i]	1 step
2	5. i:. i<\|\|l\|\| & x = l[i] i:. i<\|\|[a / l]\|\| & x = [a / l][i]	3 steps