[
  "�\u001d��9�\\�=���8\"\n�",
  [
    [
      "Vale.Curve25519.Fast_lemmas_internal.lemma_mul_pow2_bound",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_6161103b5d8ff67ff3c6e4753e084441"
      ],
      0,
      "5cb461e443313632b7e60eaf26d0f58c"
    ]
  ]
]