We study the theory of contextual equivalence in the untyped
lambda-calculus, generated by taking the normal forms as observables.
Introduced by Morris in 1968, this is the original extensional lambda
theory H+ of observational equivalence. On the syntactic side, we show
that this lambda-theory validates the omega-rule, thus settling a
long-standing open problem. On the semantic side, we provide
sufficient and necessary conditions for relational graph models to be
fully abstract for H+. We show that a relational graph model captures
Morris's observational pre-order exactly when it is extensional and
lambda-König. Intuitively, a model is lambda-König when every
lambda-definable tree has an infinite path which is witnessed by some
element of the model.