Nuprl - Proof: concat map upto 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: concat map upto 2 1

1. T : Type
2. f :

(T List)
3. t :

4. t' :

5. t<t'

map(f;upto(t+1))

map(f;upto(t'))

By:	BackThru Thm* f:(AB), L1,L2:A List. L1 L2 map(f;L1) map(f;L2)

Generated subgoal:

1 upto(t+1) upto(t')
1 step

About:

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