let rec map f xs =
    match xs with
    | [] -> []
    | hd::tl -> (f hd)::(map f tl)

map_cps f l k =
        match l with
        | [] -> k []
        | hd::tl -> map_cps f tl (fun r -> k((f hd)::r))

For all lists xs, functions f, and continuations k, prove that:
map_cps f xs k == k (map f xs)

(
 In English: at any step of the computation, the cps-converted
 map does the same thing as calling that step's continuation on
 the result of the original map on the remaining subproblem.
 
 In weaker form but simpler English:
 map_cps f l id does the same thing as map f l
)

Proof by induction over the structure of xs,
in 2 cases: xs=[] and xs=xhd::xtl 

Case xs = []
     Pick an arbitrary continuation k.
     IMS: map_cps f [] k == k(map f [])
  
(1)     map_cps f [] k                             LHS
(2) ==  k []                                       eval map_cps
(3) ==  k (map f [] )                              inv. eval map

Case xs = xhd::xtl
     Pick an arbitrary continuation k.
     IMS: map_cps f xhd::xtl k == k(map f xhd::xtl)
     IH : map_cps f xtl k == k(map f xtl)

(1)     map_cps f xhd::xtl k                       LHS
(2) ==  match xhd::xtl with ...                    Eval map_cps
(3) ==  map_cps f tl (fun r -> k((f xhd)::r))      Eval match
(4) ==  (fun r -> k((f xhd)::r)) (map f xtl)       IH
(5) ==  k((f xhd)::(map f xtl))                    eval ((map f xtl) as r)
(6) ==  k(map f hd::tl)                            inv. eval map

QED