Existential quantifications over multiple variables behaves oddly

Hi,

I just ran into the following issue: discharging by Z3 a proposition consisting of one existential quantification over two variables fails while the same proposition spelled out using two existential quantifications succeeds.

Here is a minimal example for that bug, with propositions on `int`s:
```fstar
module Bug
open FStar.Tactics

// one existential quantification over two variables (`p2` below) is
// different from two extistential quantifications over one variable
// each (`p1` below)

let p1 = exists (x: int). exists (y: int). 0 == x + y
let p2 = exists (x: int) (y: int). 0 == x + y

// even if `p1 <==> p2`
let _ = assert (p1 <==> p2)
let _ = assert p1 // `p1` is discharged successfully
[@expect_failure] // `p2` is not
let _ = assert p2

// `p2` can still be proven true by turning it manually into `p1`:
let lemma #a p
: Lemma (requires exists (x: a). exists (y: a). p x y)
(ensures exists (x: a) (y: a). p x y)
= ()
let _ = assert p2 by (apply_lemma (`lemma))
```

Has anyone run into the same issue?

Thank you!

Start by reproducing the issue with the minimal Bug module and compare Z3 discharge of p1 and p2. Investigate the existential-quantification handling involved in assert and confirm that the multi-variable form is discharged like the nested form without the manual lemma transformation.

Written by the indexing model from the issue text.