T,T':Type, a:T List, f,g:(TT').
  (x:T. (x  a)  f(x) = g(x))  map(f;a) = map(g;a)

1

1. T : Type 2. T' : Type 3. a : T List 4. f : TT' 5. g : TT' 6. x:T. (x  a)  f(x) = g(x)   map(f;a) = map(g;a)

3 steps

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