Evaluation of functions polymorphic over multiple types is bugged

[lazear]

Describe the bug
The term:

let poly = \X \Y (\func: X->Y. \val: X. func val) in poly [Nat][Bool]

evaluates to:

(λfunc: (Nat->Nat). (λval: Nat. (func val)))

when instead it should evaluate to:

(λfunc: (Nat->Bool). (λval: Nat. (func val)))

Note that the typechecker properly types this term as

((Nat->Bool)->(Nat->Bool))

To Reproduce
Steps to reproduce the behavior:

1. Type the term in the REPL
2. Evaluate

Expected behavior
Term should evaluate correctly

Additional context
It seems likely that the bug is residing in the TyTermSubst visitor. I attempted to model this off of Pierce's tmmap function, but upon further inspection I don't think it directly translates. The OCaml parser doesn't separate out TmVar and TyVar de Bruijn indices, and we do