Assertion failure when arguments are filled in via unification

````fstar
module Bug
open Pulse.Lib.Pervasives
open FStar.Mul
open FStar.FunctionalExtensionality
module SZ = FStar.SizeT

let rec bigstar (m : nat) (n : nat {m <= n}) (f : (i:nat { m <= i /\ i < n } -> vprop)) : Tot vprop (decreases n - m) =
if m = n then emp else f m ** bigstar (m+1) n f

type matrix (m n : nat) = Fin.under m ^-> Fin.under n ^-> int

let pts_to_matrix_fun (p: array int) (#m: nat) (#n: nat) (a: matrix m n) (i:nat { i < m }) : vprop = emp
let pts_to_matrix (p: array int) (#m: nat) (#n: nat) (a: matrix m n) : vprop = bigstar 0 m (pts_to_matrix_fun p a)

```pulse
ghost fn unfold_pts_to_matrix (p: array int) (#m: nat) (#n: nat) (a: matrix m n)
requires pts_to_matrix p a
returns _:unit
ensures bigstar 0 m (pts_to_matrix_fun p a)
{
rewrite pts_to_matrix p a as bigstar 0 m (pts_to_matrix_fun p a)
}
```

```pulse
fn matrix_idx (p: array int) (#m: erased nat) (#n: erased nat) (i : SZ.t { SZ.v i < m }) (a: erased (matrix m n))
requires pts_to_matrix p a
returns x:int
ensures emp
{
unfold_pts_to_matrix _ _;
admit ();
}
```
````

The last function fails with:
```
- ASSERTION FAILURE: Bound term variable not found uu___#884 in environment: ...,bigstar, x#1044, x#1043, x#1042, x#1041, x#1040
F* may be in an inconsistent state.
Please file a bug report, ideally with a minimized version of the program that triggered the error.
- See also (1,0-1,0)
Bug.fst(1, 1): related location
```