[
  "!��&\u0018�9�L\u0010E��e�",
  [
    [
      "Arch.Types.lemma_equality_check_helper_2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "fuel_guarded_inversion_Words_s.four",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
        "primitive_Prims.op_Equality", "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Words_s.Mkfour_hi2",
        "projection_inverse_Words_s.Mkfour_hi3",
        "projection_inverse_Words_s.Mkfour_lo0",
        "projection_inverse_Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "dca0e46403b3c7a27f2a9142a0a611dc"
    ],
    [
      "Arch.Types.le_bytes_to_nat64_to_bytes",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "ba8767c3e1a4654752d869b321f527a0"
    ],
    [
      "Arch.Types.le_nat64_to_bytes_to_nat64",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Words_s.nat8",
        "refinement_interpretation_Tm_refine_a38ba213f7d10ad82997d9720a14fea1"
      ],
      0,
      "2dd78f8690346deaa340e7e278c95f0f"
    ],
    [
      "Arch.Types.le_bytes_to_seq_quad32_empty",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "1af38f21f5fb7f0efa68eef0ed824728"
    ],
    [
      "Arch.Types.le_bytes_to_seq_quad32_to_bytes_one_quad",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "85f1553686dc3513f412c688d2d19524"
    ],
    [
      "Arch.Types.le_bytes_to_seq_quad32_to_bytes",
      1,
      1,
      0,
      [
        "@query", "lemma_Types_s.le_seq_quad32_to_bytes_length",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "298983f13d3bbfd41838aaed1b5d2185"
    ],
    [
      "Arch.Types.le_seq_quad32_to_bytes_to_seq_quad32",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Words_s.nat8",
        "refinement_interpretation_Tm_refine_6524c0da17dd0f4c8831555b7433a460"
      ],
      0,
      "1bcce920a159f84815e62deebfc82bf4"
    ],
    [
      "Arch.Types.le_quad32_to_bytes_to_quad32",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Words_s.nat8",
        "refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b"
      ],
      0,
      "959698b8a84122f5015944e7c8bf5732"
    ],
    [
      "Arch.Types.seq_to_four_LE_is_seq_to_seq_four_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Words.Seq_s.seq4",
        "equation_Words.Seq_s.seqn", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
      ],
      0,
      "0318facf549b30b859fcc78494312438"
    ],
    [
      "Arch.Types.le_bytes_to_seq_quad_of_singleton",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Words_s.nat8",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b"
      ],
      0,
      "e092475d8f9579c4517985c36cd74e02"
    ],
    [
      "Arch.Types.le_bytes_to_quad32_to_bytes",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "953fe17b91b86d4ba7e600acc6e292e2"
    ],
    [
      "Arch.Types.be_quad32_to_bytes",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Words.Seq_s_interpretation_Tm_arrow_32fd87de6c9aed0237ad2236679eb1c2",
        "equation_Collections.Seqs_s.compose",
        "equation_Collections.Seqs_s.seq_map", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words.Seq_s.seq4",
        "equation_Words.Seq_s.seq_four_to_seq_BE",
        "equation_Words.Seq_s.seqn", "equation_Words_s.nat32",
        "equation_Words_s.nat8",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32",
        "function_token_typing_Words_s.nat8", "int_inversion", "int_typing",
        "kinding_Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_37e29e1c3dd347eb60f455ae3b4c7ac1",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f718497de94ca05cd506a03268a8384c",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_19e63f257145a6245afb420a6f5b6b24",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Words.Seq_s.four_to_seq_BE"
      ],
      0,
      "9761aa529be04c070ff0c3a5a72ecc72"
    ],
    [
      "Arch.Types.be_bytes_to_quad32_to_bytes",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Arch.Types.be_quad32_to_bytes",
        "equation_Words.Seq_s.seq16", "equation_Words.Seq_s.seqn",
        "equation_Words_s.nat8",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "typing_Arch.Types.be_quad32_to_bytes"
      ],
      0,
      "78686287fe820bfce76e25f90c2eb1d1"
    ],
    [
      "Arch.Types.slice_commutes_seq_four_to_seq_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Words.Seq_s_interpretation_Tm_arrow_32fd87de6c9aed0237ad2236679eb1c2",
        "equation_Prims.nat", "equation_Words.Seq_s.seq_four_to_seq_LE",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "kinding_Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44a2e9e3677295a90552af8f8609c725",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_e1dced068814855698ccd7f8a4718a51",
        "refinement_interpretation_Tm_refine_f718497de94ca05cd506a03268a8384c",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_e17010ae1f40f6860845e34b0c21d194",
        "typing_Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "36a3b8f9607c3dd82c30fce1ae79d15d"
    ],
    [
      "Arch.Types.slice_commutes_le_seq_quad32_to_bytes",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "lemma_Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b"
      ],
      0,
      "43f24e371d5355b1387d18aae19285e1"
    ],
    [
      "Arch.Types.slice_commutes_le_seq_quad32_to_bytes0",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "lemma_Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b"
      ],
      0,
      "392b84f8b2377162c8d4e1ca7e915b8b"
    ],
    [
      "Arch.Types.append_distributes_le_bytes_to_seq_quad32",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Words_s.nat8",
        "function_token_typing_Words_s.nat8",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_6524c0da17dd0f4c8831555b7433a460"
      ],
      0,
      "2f6d76faab73ad0292539109512ca95c"
    ]
  ]
]