[
  "��k�5�w�q��\u0007�o�%",
  [
    [
      "Vale.Curve25519.FastSqr_helpers.lemma_dbl_pow2_six",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Curve25519.Fast_defs.pow2_five",
        "equation_Vale.Curve25519.Fast_defs.pow2_four",
        "equation_Vale.Curve25519.Fast_defs.pow2_six",
        "equation_Vale.Curve25519.Fast_defs.pow2_three",
        "equation_Vale.Curve25519.Fast_defs.pow2_two", "int_inversion",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "83a728e61b537dec5681873f7fc47ed7"
    ],
    [
      "Vale.Curve25519.FastSqr_helpers.lemma_sqr_part3",
      1,
      0,
      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,
      "26cbc852d3cc0dbc7fb1b7f4aa0b14da"
    ],
    [
      "Vale.Curve25519.FastSqr_helpers.lemma_sqr_part3",
      2,
      0,
      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.Curve25519.Fast_defs.pow2_eight",
        "equation_Vale.Curve25519.Fast_defs.pow2_five",
        "equation_Vale.Curve25519.Fast_defs.pow2_four",
        "equation_Vale.Curve25519.Fast_defs.pow2_nine",
        "equation_Vale.Curve25519.Fast_defs.pow2_seven",
        "equation_Vale.Curve25519.Fast_defs.pow2_six",
        "equation_Vale.Curve25519.Fast_defs.pow2_three",
        "equation_Vale.Curve25519.Fast_defs.pow2_two",
        "equation_Vale.Def.Types_s.add_wrap",
        "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",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "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",
        "typing_Vale.Def.Types_s.add_wrap"
      ],
      0,
      "3f5369a64367c7a5174487ed4c2d4bb2"
    ],
    [
      "Vale.Curve25519.FastSqr_helpers.lemma_sqr",
      1,
      0,
      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,
      "f805084322fc904d56f5c402dd2e85c2"
    ],
    [
      "Vale.Curve25519.FastSqr_helpers.lemma_sqr",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Curve25519.Fast_defs.bit",
        "equation_Vale.Curve25519.Fast_defs.mul_nats",
        "equation_Vale.Curve25519.Fast_defs.pow2_eight",
        "equation_Vale.Curve25519.Fast_defs.pow2_five",
        "equation_Vale.Curve25519.Fast_defs.pow2_four",
        "equation_Vale.Curve25519.Fast_defs.pow2_nine",
        "equation_Vale.Curve25519.Fast_defs.pow2_seven",
        "equation_Vale.Curve25519.Fast_defs.pow2_six",
        "equation_Vale.Curve25519.Fast_defs.pow2_three",
        "equation_Vale.Curve25519.Fast_defs.pow2_two",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "int_typing", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b51b45ce195a33a465eab411d92fdae9",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "true_interp", "typing_Vale.Curve25519.Fast_defs.mul_nats",
        "typing_Vale.Curve25519.Fast_defs.pow2_eight",
        "typing_Vale.Curve25519.Fast_defs.pow2_four"
      ],
      0,
      "0728d9d1171009bbe055a3a83d1e632a"
    ],
    [
      "Vale.Curve25519.FastSqr_helpers.lemma_sqr",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_8caf45e0aed18c9b62d4d95913588c9d"
      ],
      0,
      "98554bf435804403051426fae894f628"
    ],
    [
      "Vale.Curve25519.FastSqr_helpers.lemma_sqr",
      4,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Curve25519.Fast_defs.mul_nats",
        "equation_Vale.Curve25519.Fast_defs.pow2_five",
        "equation_Vale.Curve25519.Fast_defs.pow2_four",
        "equation_Vale.Curve25519.Fast_defs.pow2_seven",
        "equation_Vale.Curve25519.Fast_defs.pow2_six",
        "equation_Vale.Curve25519.Fast_defs.pow2_three",
        "equation_Vale.Curve25519.Fast_defs.pow2_two",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_27a1c633e5003b2ca3926b3e117bb4a9",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8caf45e0aed18c9b62d4d95913588c9d",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_f7b2ab877c5f6d385696d70a27ca46b3"
      ],
      0,
      "527fae6371bb1d36ff5cab30c35f3ebe"
    ],
    [
      "Vale.Curve25519.FastSqr_helpers.lemma_sqr",
      5,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0cc3b8bc4390a8152398abb544530a43"
      ],
      0,
      "748d7078c443481c20a5aa221c708304"
    ]
  ]
]