Prop 11, item 1 is wrong: it requires the property 

   \x.C-(\_.k x) M -> C-(\_.k M)

which is false in CBV. A correct (and weaker) statement is

Prop 11. 1. Given \_v-C terms M and N, if M -> N then
doublelineover{M} ~= doublelineover{N},

where ~= is operational equivalence in \-{C-}-top defined by M ~= N
iff for all substitution sigma of the free term and continuation
variables of M and N (top included) and for all context E, E[M sigma]
-> V_1 iff E[N sigma] -> V_2 for some values V_1 and V_2.