Incorrect higher order counterexample from Nebula

[BillHallahan]

On master, running:

time cabal run Nebula tests/RewriteVerify/Correct/TestZeno.hs p12

results in a generated (incorrect) counterexample:

--------------------
COUNTEREXAMPLE FOUND
--------------------
Left Path: Start -> a0 -> a4 -> a14
Right Path: Start -> b1 -> b5 -> b16
drop Z (map f'5 ((fs'4:fs'3))) = : _ (TICK[__ERROR_LABEL__'1]{error}) _ but map f'5 (drop Z ((fs'4:fs'3))) = : _ (TICK[__ERROR_LABEL__]{error}) _
Main Symbolic Variables:
f'5 = Symbolic T'3 -> T
xs = : @T'3 fs'4 fs'3
fs'4 = Symbolic T'3
fs'1 = TICK[__ERROR_LABEL__]{error}
fs = TICK[__ERROR_LABEL__'1]{error}
fs'3 = Symbolic ([] T'3)
a'112 = @T'1
f'5 = Symbolic T'3 -> T
n'21 = Z
a'110 = @T'2
Symbolic Function Mappings:
f'5 fs'4 --> fs'1
f'5 fs'4 --> fs
SAT ()

This appears to be caused by instType. If line 603 in G2.Interface.Interface:
https://github.com/BillHallahan/G2/blob/master/src/G2/Interface/Interface.hs#L603
is replaced with:

    let (ng'',exec_states') = (name_gen bindings', exec_states) -- L.mapAccumL instType (name_gen bindings') exec_states

Nebula is able to (correctly) prove the property.