This code was generated with the following toolchain.
F* version: 8e5d6706f355598341869d3057cfa8228c90a51d
KreMLin version: 44acff92da5e2483675a9946e3a4ab21cb617aa9
Vale version: 0.3.10