[
  "o?0V°ÆÁp`( \u0016}—Z4",
  [
    [
      "Vale.Curve25519.FastSqr_helpers.lemma_sqr_part3",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "eq2-interp",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Prims.squash",
        "equation_Vale.Curve25519.Fast_defs.add_carry",
        "equation_Vale.Curve25519.Fast_defs.bit",
        "equation_Vale.Curve25519.Fast_defs.mul_nats",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "l_and-interp", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b51b45ce195a33a465eab411d92fdae9",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "773114f7b82689a4455a43ceee7fe159"
    ],
    [
      "Vale.Curve25519.FastSqr_helpers.lemma_sqr",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Curve25519.Fast_defs.mul_nats",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Curve25519.Fast_defs.mul_nats"
      ],
      0,
      "bf1cb0ac382347b213a4739fb1bd0386"
    ]
  ]
]