rewrite each could match types on each side

[mtzguido]

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.