[
  "ùÔ\u001c$ÃM³Óì~~êIm—{",
  [
    [
      "Vale.Bignum.Lemmas.seq_add_c",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_9a3bf8082924c76056d4f6da1c781914_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_cd266facd57b554ccc93fa79ab54a348_1", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.natN",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "well-founded-ordering-on-nat"
      ],
      0,
      "4bec71fe835531f73e9eacb9f28f6418"
    ],
    [
      "Vale.Bignum.Lemmas.seq_add_i",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "7bfd552cf8d25cfdeabae89d367daa83"
    ],
    [
      "Vale.Bignum.Lemmas.seq_add",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Vale.Bignum.Lemmas_interpretation_Tm_arrow_c3d5b4c9a207f9ca5ebaa34010b705a3",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat1",
        "equation_Vale.Def.Words_s.natN", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cbe95f5a2b690e6ac92cc19518cf1415",
        "typing_FStar.Seq.Base.length", "typing_Vale.Def.Words_s.natN"
      ],
      0,
      "6415ed885ac9ff022ea584a1edaeb949"
    ],
    [
      "Vale.Bignum.Lemmas.seq_scale_lo",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "e62f428b47a283f9709c0fc63e1889f6"
    ],
    [
      "Vale.Bignum.Lemmas.seq_scale_lo",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Vale.Bignum.Lemmas_interpretation_Tm_arrow_59eaa5277515751de303a597beb3dd4a",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_init_len", "primitive_Prims.op_Equality",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_bb4a9973c8f99b57985a81227273102e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "20759dd3ebf9880256d488fcfa9e3a63"
    ],
    [
      "Vale.Bignum.Lemmas.seq_scale_hi",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "0f87dc1aac5f35f990f5f3bc01656838"
    ],
    [
      "Vale.Bignum.Lemmas.seq_scale_hi",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Bignum.Lemmas_interpretation_Tm_arrow_59eaa5277515751de303a597beb3dd4a",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Vale.Def.Words_s.natN",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "lemma_FStar.Seq.Base.lemma_init_len",
        "primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_bb4a9973c8f99b57985a81227273102e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "95225607be0643111116dcbc87eeea61"
    ],
    [
      "Vale.Bignum.Lemmas.seq_scale",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "2cc10942e1d9397e385670b509684671"
    ],
    [
      "Vale.Bignum.Lemmas.seq_scale",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "equation_FStar.Pervasives.Native.fst", "equation_Prims.pos",
        "equation_Vale.Def.Words_s.nat1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "e57ccf5b77b52f4ed2ab000400ff099c"
    ],
    [
      "Vale.Bignum.Lemmas.lemma_sum_seq_left_right",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
        "equation_Prims.squash", "l_and-interp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "0f0bc9b2acae3626891ef82e30b093a9"
    ],
    [
      "Vale.Bignum.Lemmas.seq_add_is",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_9a3bf8082924c76056d4f6da1c781914_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_cd266facd57b554ccc93fa79ab54a348_1",
        "equation_FStar.Pervasives.Native.fst", "equation_Prims.l_True",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.natN",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.l_True", "int_inversion", "int_typing",
        "primitive_Prims.op_Equality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "well-founded-ordering-on-nat"
      ],
      0,
      "e14a50455b51df6074f8b1c743b72a6e"
    ],
    [
      "Vale.Bignum.Lemmas.seq_add_is_norm",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "5f9894934174e6614581578466e0bb5b"
    ],
    [
      "Vale.Bignum.Lemmas.lemma_seq_add_is_norm",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "eq2-interp",
        "equation_Prims.l_and", "equation_Prims.nat",
        "equation_Prims.squash", "l_and-interp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "2263b17237f9d822198424f977d27ace"
    ],
    [
      "Vale.Bignum.Lemmas.lemma_seq_add",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
        "equation_Prims.nat", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "5cfc93f5e808a8c3f99c2af24f3c4434"
    ],
    [
      "Vale.Bignum.Lemmas.lemma_seq_scale_carry",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "ed8906dbb0d352db97d3ca10e23f18fb"
    ],
    [
      "Vale.Bignum.Lemmas.lemma_seq_scale",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "ca3fbea509098579a9d15014452020f7"
    ],
    [
      "Vale.Bignum.Lemmas.ys_init",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.natN",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_bb4a9973c8f99b57985a81227273102e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_FStar.Seq.Base.length", "typing_Vale.Def.Words_s.natN"
      ],
      0,
      "b3bee613f9f3eb403a03838d2a76587d"
    ],
    [
      "Vale.Bignum.Lemmas.zs_init",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.natN", "int_inversion",
        "primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_bb4a9973c8f99b57985a81227273102e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "cbe841bed3ef9997ee50ec6df11d6363"
    ],
    [
      "Vale.Bignum.Lemmas.init_ys",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.Seq.Base.length", "typing_Vale.Def.Words_s.natN"
      ],
      0,
      "33ad93177b190a4eb02624404c5f8d15"
    ],
    [
      "Vale.Bignum.Lemmas.init_zs",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.Seq.Base.length", "typing_Vale.Def.Words_s.natN"
      ],
      0,
      "d2e1badfc40aaa327f96022bb91cf801"
    ],
    [
      "Vale.Bignum.Lemmas.lemma_scale_add",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Bignum.Lemmas_interpretation_Tm_arrow_9cecc1e6381aab8ddca91566689c42b6",
        "eq2-interp", "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.natN",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_64c7cdf80f5eb0b5f10cf9506fa04793",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_FStar.Seq.Base.length", "typing_Vale.Def.Words_s.natN"
      ],
      0,
      "e2045a10082105c271065a8ebebf2da0"
    ]
  ]
]