change the order of substitution variables from
    x$ |-> x |-> e
to
    x |-> x$ |-> e
because in LF, the type of x$ (which is something like "hastype x T")
depends on x.