Matching on erased

[mtzguido]

This snippet

```pulse
ghost
fn test (x : erased int)
  requires emp
  ensures  emp
{
  match x {
    0 -> {
     ();
    }
    _ -> {
     ();
    }
  }
}
```

fails with:

* Error 228 at MatchBug.fst(5,12-5,12):
  - Cannot type
      match x with
      | 0 -> 1
      | _ -> 1
    in context [(x: FStar.Ghost.erased Prims.int)]
  - Type of pattern (Prims.int) does not match type of scrutinee (FStar.Ghost.erased Prims.int)
  - See also Pulse.Checker.Match.fst(431,10-431,64)

1 error was reported (see above)

with a bad range, pointing to right after the pulse label. The fix is to do let xx = reveal x; before the match and match on xx, but that's not at all obvious from the error. Further the reveal could be automatic as we are in a ghost context.