Nuprl - Proof: before-map 2 1 1 1

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

1. T : Type
2. T' : Type
3. f : T

T'
4. T List
5. u : T
6. v : T List
7.

x',y':T'.
7. x' before y'

map(f;v)

(

x,y:T. x before y

v & f(x) = x' & f(y) = y')
8. x' : T'
9. y' : T'
10. x' = f(u)
11. y : T
12. (y

v)
13. y' = f(y)

x,y:T. x = u & (y

x before y

v & f(x) = x' & f(y) = y'

By:	InstConcl [u;y] THEN OrLeft

Generated subgoals:

None

About:

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