This code was generated with the following toolchain.
F* version: 39375e7bf186b7b7da4ac34c6076b9bd9d57d28d
KreMLin version: 504500d9d25b7098a2c65207c982898bd8566f5e
Vale version: 0.3.13
