rewrite each could match types on each side

```fstar
let foo (x : list 'a) : slprop = emp

fn test ()
requires foo [1]
ensures emp
{
rewrite each [1] as [2];
drop_ (foo [2]);
}

fn test2 ()
requires foo [1]
ensures emp
{
rewrite each [1] as [];
drop_ (foo []);
}
```
The rewrite in `test2` fails to work as we cannot resolve the type of the Nil constructor in the RHS of the rewrite, but it should be `int`, to match the LHS.

No file or test is named. Reproduce the `test2` example with `rewrite each [1] as []` and compare it with `test`; trace type resolution for the RHS `Nil` constructor. Done means the RHS resolves to `int` and the rewrite succeeds.

Written by the indexing model from the issue text.