We discuss {\em new} ways of characterizing, as {\em maximal fixed points} of
monotone operators, observational congruences on $\lambda$-terms and, more
generally, equivalences on applicative structures. These characterizations
naturally induce {\em new} forms of {\em coinduction principles}, for 
reasoning on program equivalences, which are not based on Abramsky's 
{\em applicative bisimulation}. 

We discuss in particular, what we call, the {\em cartesian} coinduction
principle, which arises when we exploit the elementary observation that 
functional behaviours can be expressed as {\em cartesian graphs}. 
 
Using the paradigm of final semantics, the soundness of this principle over an
applicative structure can be expressed easily by saying that the applicative 
structure can be construed as a {\em strongly extensional coalgebra} for the 
functor $({\cal P}(\ \_ \times\ \_)) \oplus ({\cal P}(\ \_ \times\ \_))$. 

In this paper, we present two general methods for showing the soundenss of 
this principle. 
The first applies to {\em approximable applicative structures}.
Many CPO $\lambda$-models in the literature, and the corresponding quotient
models of indexed terms turn out to be approximable applicative structures.
The second method is based on Howe's congruence candidates, and it applies to
many observational equivalences.

Structures satisfying  cartesian coinduction are precisely those applicative 
structures which can be modeled using the standard {\em set-theoretic}
application in non-wellfounded theories of sets, where the Foundation Axiom is
replaced by the Axiom $X_1$ of Forti and Honsell.