[
  "gCœ\u0016H_\u001dgŠPŸ»Ú1&’",
  [
    [
      "Vale.Curve25519.Fast_lemmas_internal.lemma_mul_bounds_le",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "c610aa3ce085c740e17121c2fe407c81"
    ],
    [
      "Vale.Curve25519.Fast_lemmas_internal.lemma_mul_pow2_bound",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_6161103b5d8ff67ff3c6e4753e084441"
      ],
      0,
      "e4cd1f8392ebf77b8486aa7d355a6de5"
    ],
    [
      "Vale.Curve25519.Fast_lemmas_internal.lemma_mul_pow2_bound",
      2,
      1,
      0,
      [ "@query" ],
      0,
      "ddac90ae96a03e27d292478b0d22b77e"
    ],
    [
      "Vale.Curve25519.Fast_lemmas_internal.lemma_mul_pow2_bound",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Vale.Def.Words_s.natN",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6161103b5d8ff67ff3c6e4753e084441",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Prims.pow2"
      ],
      0,
      "8b6cb90d77687755e952a89cf2e5cd28"
    ],
    [
      "Vale.Curve25519.Fast_lemmas_internal.lemma_mul_bound64",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "f85df6b1d25102baf2b1c1dacd095717"
    ],
    [
      "Vale.Curve25519.Fast_lemmas_internal.lemma_intel_prod_sum_bound",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "c9952af49b927656467ca38f4f22909d"
    ],
    [
      "Vale.Curve25519.Fast_lemmas_internal.lemma_double_bound",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.Def.Types_s.add_wrap",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "739c7278950303bd7aee22fbc2119085"
    ]
  ]
]