Variants on custom relations always introduce polymorphism
Using custom relations in variant triggers the use of the Wellfounded module, which itself introduces polymorphism in tasks. Would it be possible to ignore this polymorphism, or to make a monomorphic clonable module Well_founded?
Incidentally, the goal is to write loop on bitvector variables, and not using the 'to_int to prove decreasingness but directly BV.sgt
.