Expected type of arguments not (always?) useds

This works fine:
```fstar
fn use_nat (x : nat) { () }
fn call_nat () { use_nat 42; }
```

But,
```fstar
fn use_nat (x : nat & nat) { () }
fn call_nat () { use_nat (42, 1); }
```
Gives:
```
- Ill-typed term: FStar.Pervasives.Native.Mktuple2 #int #nat 42 1
- Expected a term of type nat & nat
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more details.
- Also see: /home/guido/r/kuiper/main/inst/lib/fstar/ulib/Prims.fst:161.28-183.79
- Raised within Tactics.refl_core_check_term
F*
- This query failed:
- forall (i: Prims.int) (x: Prims.unit).
Prims.trivial <==> Prims.equals #Prims.bool (i >= 0) true
F*
```
Likely since we've elaborated the tuple without regard for the expected type.

It is even the case when it's not the last argument.
```fstar
fn use_nat (x : nat & nat) () { () }

fn call_nat () { use_nat (42, 1) (); }
```
```
- Ill-typed term: use_nat (FStar.Pervasives.Native.Mktuple2 #int #nat 42 1)
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more details.
- Also see: /home/guido/r/kuiper/main/inst/lib/fstar/ulib/Prims.fst:161.28-183.79
- Raised within Tactics.refl_tc_term
F*
- This query failed:
- forall (i: Prims.int) (x: Prims.unit).
Prims.trivial <==> Prims.equals #Prims.bool (i >= 0) true
```

Note that, somehow, in the last two cases the second type was inferred to be `nat`... unsure why.

Reproduce the reported examples involving tuple arguments expected to have type nat & nat, including the case where the tuple is not the last argument. Trace tuple elaboration and expected-type propagation in the F* type-checking path; done means all examples type-check correctly without the reported SMT errors.

Written by the indexing model from the issue text.