T,T':Type, a:T List, f,g:(TT').
  (i:. i<||a||  f(a[i]) = g(a[i]))  map(f;a) = map(g;a)

1

1. T : Type 2. T' : Type 3. a : T List 4. f : TT' 5. g : TT' 6. i:. i<||a||  f(a[i]) = g(a[i])   map(f;a) = map(g;a)

5 steps

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