Coinductive (applicative) characterizations of various observational congruences
which arise in the semantics of $\lambda$-calculus, for various reduction
strategies, are discussed. Two semantic techniques for establishing the
coincidence of the applicative and the contextual equivalences are analyzed.
The first is based on {\em intersection types}, the second is based on a 
{\em mixed induction-coinduction principle}.