[
  "wˆ>“=rôBÝ&Qüµ¢±Ø",
  [
    [
      "Vale.Curve25519.FastUtil_helpers.sub_carry",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Curve25519.Fast_defs.bit",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b51b45ce195a33a465eab411d92fdae9",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "2b0d7e2abe138ea6eb14f0970afa4d22"
    ],
    [
      "Vale.Curve25519.FastUtil_helpers.lemma_sub3",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "5af7469ca8a475e3b3b4d15ad369299a"
    ],
    [
      "Vale.Curve25519.FastUtil_helpers.lemma_sub",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "5444cad3125f79d8d323f01b42c6030f"
    ]
  ]
]