Higher-order assumption fails for `tm-of-reg`

Consider the following theorem. https://github.com/MartyO256/mechanizing-standard-ml/blob/dcb3c22b93995a727cd5dfcfcbce9542c7efd627/src/safety/regularity.thm#L2756-L2772 This is not exactly a translation of tm-of-reg from the original mechanization since it requires an alternating schema that uses termbind-reg. However, the higher-order assumption u : {F' : sttp} tm-of F' x T is mishandled in Harpoon.

In the issue2 branch, execute the following commands.

harpoon --sig ./src/sources.cfg
select tm-of-reg
split x
session serialize

Upon type reconstruction, the following error is thrown.

./src/./safety/regularity.thm, line 3087, column 7:
Type-checking error.
Ill-typed expression.
    Expected type:
      [?g[^0] |-
         tm-of (?F_43703[^0][..]) (?E_43704[^0][..]) (?T_43705[^0][..])]
    Inferred type:
      [?g[^0] |-
         {F' : sttp}  tm-of F' (?#tof_43708.1[^0][..]) (?C478_43706[^0][..])]

This refers to the assumption case, serialized as follows.

case #.2:
{ g : termbind-reg,
  F : ( |- sttp),
  T : (g |- con),
  #tof : #(g |- block (x : term, u : {F' : sttp}  tm-of F' x (T[..]))),
  Dof155 : (g |- cn-of T t)
| x : [g |- tm-of F[] #tof.1 T]
; solve [_ |- Dof155]
}

The issue is to either revise the definition of termbind-reg, or to investigate why Harpoon yields that erroneous assumption case.

MartyO256 / mechanizing-standard-ml

Higher-order assumption fails for `tm-of-reg` #2