"intLib.ARITH_PROVE ``0n = x * Num 0i``" fails unexpectedly

[someplaceguy]

While working on Z3 proof replay in HolSmt, I came across this unexpected failure in intLib.ARITH_PROVE:

> intLib.ARITH_PROVE ``0n = x * Num 0i``;
Exception-
   HOL_ERR
     {message = "EXISTS_AND_CONV: `x` free in both conjuncts",
      origin_function = "RAND_CONV", origin_structure = "Conv"} raised

However, the following similar proof attempts do seem to work fine:

> intLib.COOPER_PROVE ``0n = x * Num 0i``;
> intLib.ARITH_PROVE ``x = x * Num 1i``;
> intLib.ARITH_PROVE ``0n = x * 0n``;
> intLib.ARITH_PROVE ``0n = Num 0i``;

After discussion in the #hol4 Discord channel confirming this was a bug in HOL4, I was instructed to file this issue.

Thanks!

[someplaceguy]

Similar failures:

> intLib.ARITH_PROVE ``0i = &x * &Num 0``
> intLib.ARITH_PROVE ``0i = &Num 0 * &x``