A,B:Type, f:(AB), as,as':A List.
  map(f;as @ as') = (map(f;as) @ map(f;as'))

1

1. A : Type 2. B : Type 3. f : AB 4. as : A List 5. as' : A List   map(f;as @ as') = (map(f;as) @ map(f;as'))

3 steps

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