Explicit type required for tuple result of choose

[jaylorch]

In the docs (specifically, source/docs/guide/src/exists.md), it says:

TODO: `(x, y)` should not require the type annotation `: (int, int)`

for the following code:

spec fn less_than(x: int, y: int) -> bool {
    x < y
}

proof fn test_choose_succeeds2() {
    assert(less_than(3, 7));  // promote i = 3, i = 7 as a witness
    let (x, y): (int, int) = choose|i: int, j: int| less_than(i, j);
    assert(x < y);
}

We should fix that, and then remove the TODO from the docs.