Locally nameless failure

[mtzguido]

This fragment:

let is_list #t  (l:list t)
  : Tot vprop (decreases l)
  = match l with
    | [] -> emp
    | ns -> emp

```pulse
ghost
fn unfold_is_list_cons (#t:Type0) (xs : (list t))
  requires is_list xs
  returns  _:unit
  ensures  emp
{
  unfold (is_list xs);
  match xs {
    Cons hd tl -> {
      rewrite each xs as Cons hd tl;
      admit();
    }
    Nil -> {
      admit();
    }
  }
}
```

Fails (crashes, we could say) with:

* Error <unknown> at BBB.fst(7,8-9,19):
  - Failure: not locally nameless!
  - Aborting before calling rtb_core_check_term.e
  - term
    =
    match _ :: _ with
    | Prims.Nil #_ -> Pulse.Lib.Core.emp
    | _ -> Pulse.Lib.Core.emp

* Error <unknown> at BBB.fst(7,8-9,19):
  - Expected term of type vprop
    got term
      match _ :: _ with
      | Prims.Nil #_ -> Pulse.Lib.Core.emp
      | _ -> Pulse.Lib.Core.emp

* Error <unknown> at BBB.fst(11,4-29,7):
  - FStar_Tactics_Common.TacticFailure(_)

* Error 228 at BBB.fst(11,12-11,12):
  - Pulse checker failed
  - See also Pulse.Typing.Env.fst(406,2-406,31)

4 errors were reported (see above)

Locations are also bad. This happens even before the new matcher.