Nuprl - Proof: map equal2 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: map equal2 1 1 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)
7. i :

8. i<||a||

(a[i]

By:	Unfold `l_member` 0 THEN InstConcl [i]

Generated subgoals:

None

About:

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