Nuprl - Proof: map equal2 1

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

1. T : Type
2. T' : Type
3. a : T List
4. f : T

T'
5. g : T

T'
6.

x:T. (x

f(x) = g(x)

map(f;a) = map(g;a)

By:	BackThru Thm* a:T List, f,g:(TT'). Thm* (i:. i<\|\|a\|\| f(a[i]) = g(a[i])) map(f;a) = map(g;a)

Generated subgoal:

1 7. i :
8. i<||a||
f(a[i]) = g(a[i])
2 steps

About:

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