Nuprl - Proof: member-concat 2

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

1. T : Type
2. (T List) List
3. u : T List
4. v : (T List) List
5.

x:T. (x

concat(v))

(

l:T List. (l

v) & (x

l))
6. x : T
7. l : T List
8. l = u

v)
9. (x

concat(v))

By:	Analyze -2

Generated subgoals:

1 8. l = u
9. (x  l)
  (x  u)  (x  concat(v))
1 step

2 8. (l  v)
9. (x  l)
  (x  u)  (x  concat(v))
2 steps

About:

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

1	8. l = u 9. (x l) (x u) (x concat(v))	1 step
2	8. (l v) 9. (x l) (x u) (x concat(v))	2 steps