Incomplete reasoning about exponentiation: 2^^h + 2^^h - 2^^h does not always simplify to 2^^h

[RyanGlScott]

Consider:

// See if Cryptol knows that 2^^h + (2^^h - 2^^h) == 2^^h

f : {h} (fin h) => [2^^h + (2^^h - 2^^h)]
f = g`{h}

g : {h} (fin h) => [2^^h]
g = zero

// See if Cryptol knows that (2^^h + 2^^h) - 2^^h == 2^^h

ff : {h} (fin h) => [(2^^h + 2^^h) - 2^^h]
ff = gg`{h}

gg : {h} (fin h) => [2^^h]
gg = zero

This is seeing if Cryptol can successfully conclude that 2^^h + 2^^h - 2^^h == 2^^h with different groupings of the (+) operator. Surprisingly, Cryptol succeeds in the first case (2^^h + (2^^h - 2^^h) == 2^^h), but fails in the second case ((2^^h + 2^^h) - 2^^h == 2^^h):

[error] at Bug.cry:12:1--12:12:
  Failed to validate user-specified signature.
    in the definition of 'Main::ff', at Bug.cry:12:1--12:3,
    we need to show that
      for any type h
      assuming
        • fin h
      the following constraints hold:
        • 2 ^^ (1 + h) - 2 ^^ h == 2 ^^ h
            arising from
            matching types
            at Bug.cry:12:6--12:8

Normally, Cryptol's typechecker has no problem concluding that (x + x) - x == x. As the error message above indicates, however, I think Cryptol's typechecker is getting confused because it first rewrites (2^^h + 2^^h) to 2 ^^ (1 + h), which imperils the typechecker's ability to cancel out 2^^h terms.