Two quantifiers in a specification

[vectorpikachu]

Hello, I've encountered a problem of having two quantifiers in a specification. And I have added some descriptions in the following code to demonstrate the problem I've met.
how can I make test1 lemma and test2 lemma work, without introducing another predicate?
Does the problem occur because of my misuse of Dafny, or because of some problems in Dafny itself?

Really thank you for your attention to this problem!

// Test predicate
ghost predicate P(a: seq<int>, x: int, y: int)
{
    (0 <= x < |a| && 0 <= y < |a|) ==> a[x] < a[y]
}

lemma test1(a: seq<int>)
    requires forall x :: (exists y :: P(a, x, y))
    ensures forall x :: (exists y :: P(a, x, y))
{
    // not proved
    // Dafny can't find the trigger for `x`
}

lemma test2(a: seq<int>)
    requires exists x :: (forall y :: P(a, x, y))
    ensures exists x :: (forall y :: P(a, x, y))
{

    // not proved
    // same issue as test1
}

// Using a different predicate to set triggers
ghost predicate exist_y_P(a: seq<int>, x: int)
{
    exists y :: P(a, x, y)
}

lemma test1'(a: seq<int>)
    requires forall x {:trigger (exist_y_P(a, x))} :: exist_y_P(a, x)
    ensures forall x :: exist_y_P(a, x)
{
    // proved
}

ghost predicate forall_x_P(a: seq<int>, y: int)
{
    forall x :: P(a, x, y)
}

lemma test2'(a: seq<int>)
    requires exists x :: forall_x_P(a, x)
    ensures exists x :: forall_x_P(a, x)
{
    // proved
}