#[options]
When extracting to F*, wrap this item in #push-options "..." and #pop-options.
#push-options "..."
#pop-options