Crash with extracting quotations

[mtzguido]

This crashes with "antiquotation out of bounds". Removing the open also causes a (hopefully silly) crash about term not being in the environment

open FStar.Tactics

type s (x:int) = int

let t = (`(x:int -> s x))

[mtzguido]

Related, this snippet fails but should be provable, both by normalization and SMT:

module C

open FStar.Reflection.V2

let test (f g : term) =
  assert_norm ( `( (`#f) (`#g) ) == pack_ln (Tv_App f (g, Q_Explicit)))