We give the first sound and complete proof method for observational
equivalence in full polymorphic $\lambda$-calculus with existential
types and first-class, higher-order references.  Our method is
syntactic and elementary in the sense that it only employs simple
structures such as relations on terms.  It is nevertheless powerful
enough to prove many interesting equivalences that can and cannot be
proved by previous approaches, including the latest work by Ahmed,
Dreyer and Rossberg (POPL 2009).