1. T : Type
2. a : T List
3. f : TT
4. x:T. (x  a)  f(x) = x
  map(f;a) = map(Id;a)

By:	BackThru Thm* a:T List, f,g:(TT'). Thm* (x:T. (x  a)  f(x) = g(x))  map(f;a) = map(g;a)

1

5. x : T 6. (x  a)   f(x) = Id(x)

1 step

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