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.