I think that, in most proofs of equivalence between models of computation (“a function can be computed by an automaton of type A iff it can be computed by an automaton of type B”), both directions usually offer some insight.
This is a simple but fundamental example from complexity theory. Define NP to be the class of languages (equivalently, decision problems) recognised by nondeterministic Turing machines operating in polynomial time. Then:
Theorem. A language L is in NP iff there exist a deterministic Turing machine M operating in polynomial time and a polynomial p such that, for each string x,
if x ∈ L then there exists a string y with |y| ≤ p(|p(|x|) such that M accepts (x, y);
if x ∉ L then M rejects (x, y) for all strings y with |y| ≤ p(|p(|x|).
The deterministic Turing machine M can be called a verifier, and the strings y accompanying each string x ∈ L that make M accept are called short certificates: they constitute an easily verifiable proof of membership of x in the language; no string outside L possesses such a membership proof.
For a proof of this theorem see, for instance, this page on Wikipedia; notice that both implications have an easy but not completely trivial proof.
The proof of “L has short certificates ⇒ L ∈ NP” shows how the “magic” of nondeterminism can be used to guess a certificate (if it exists for a particular input string).
The proof of “L ∈ NP ⇒ L has short certificates”, on the other hand, shows that nondeterminism, which might appear an unrealistic notion, implies the very concrete existence of short, easily checkable proofs for some properties of the input that might be too hard to decide efficiently.
