This code was generated with the following toolchain.
F* version: 86caa3d31325cec42aba32dcf17c749917720ada
KreMLin version: f3656741e080d038f5f96a2864666e58ba34b831
Vale version: 0.3.13
