I've seem two different notions of operational equivalence being used for the $\lambda$-lalculus, i.e., an equivalence stating that "if we replace term $a$ with a term $b$ in a program, the observable behavior of the program isn't changed". The first is Morris' context equivalence, which is defined, given that $v$ is a value of a ground type (bool, nat, etc):
$$a \approx_M b \iff (\forall C,\forall v,C[a]\Downarrow v \iff C[b]\Downarrow v)$$
I.e., for all possible program contexts, plugging in $a$ gives a constant $v$ iff plugging in $b$ does as well: the context can't tell them apart. The second definition I've seem is Abramsky's applicative bisimulation, which is a coindutive definition that "looks inside abstractions":
$$a \approx_A b\iff (\forall a',a\Downarrow \lambda x.a' \implies \exists b',b\Downarrow\lambda x.b' \land \forall c,a'[c/x] \approx_Ab'[c/x])$$
Abramsky's paper also states that the above definition can be characterizad as follows:
$$a\approx_Ab\iff(\forall C, C[a]\Downarrow\iff C[b]\Downarrow)$$
I.e., for all possible program contexts, plugging in $a$ halts iff plugging in $b$ also halts.
(In the above definitions, $x \Downarrow y$ is the big step operational semantics, and $x\Downarrow$ means $\exists y,x\Downarrow y$.)
These seems to me somewhat complementary (as Morris' equivalence checks for constants and Abramsky's equivalence checks under abstractions). My question is: in the $\lambda$-calculus, are these equivalences comparable? I.e., can I derive one from the other? If so, would this be preserved for typed versions of the relations, where we would have less discriminating power on contexts?
(Just to give some context on my question: I'm investigating full abstraction of the simply typed lambda calculus into the simply typed CPS-calculus, where in fact the corresponding versions of Morris' and Abramsky's equivalences coincide, at least in the untyped version. Any directions for this are welcome.)