Dafny: Proving forall x :: P(x) ==> Q(x)

The general method in Dafny for proving something of the form forall x :: P(x) ==> Q(x) is:

lemma X()
    ensures forall x :: P(x) ==> Q(x);
{
    forall x | P(x)
        ensures Q(x);
    {
       // prove Q(x)
    }
}