{\em Proof principles} for reasoning about various semantics of untyped
$\lambda$-calculus are discussed. The semantics are determined operationally by
fixing a particular {\em reduction  strategy} on $\lambda$-terms and a suitable set
of {\em values}, and by taking the corresponding {\em observational equivalence} on
terms. These principles arise naturally as co-induction principles, when the
observational equivalences are shown to be induced by the {\em unique} mapping into
a {\em final $F$-coalgebra}, for a suitable functor $F$. This is achieved either by
{\em induction on computation steps} or exploiting the properties of some,
computationally adequate, inverse limit denotational model. The final $F$-coalgebras
cannot be given, in general, the structure of a ``denotational'' $\lambda$-model. 
Nevertheless the ``final semantics'' can count as {\em compositional} \/ in that it
induces a {\em congruence}. We utilize the intuitive categorical setting of {\em
hypersets} and functions. The importance of the principles introduced in this paper
lies in the fact that they often allow to factorize the complexity of proofs (of
observational equivalence) by  ``straight'' induction on computation steps, which
are usually lengthy and error-prone.