[
  "��8e\u0016dL27N��C\f�q",
  [
    [
      "Map16.sel2",
      1,
      1,
      0,
      [ "@query", "primitive_Prims.op_LessThan" ],
      0,
      "e4c754f06e836c112573c10056b0070d"
    ],
    [
      "Map16.sel4",
      1,
      1,
      0,
      [ "@query", "primitive_Prims.op_LessThan" ],
      0,
      "63793b725aac0d8556a444fabd029fe6"
    ],
    [
      "Map16.sel8",
      1,
      1,
      0,
      [ "@query", "primitive_Prims.op_LessThan" ],
      0,
      "86fbd018bcbdd284091ef351e5adc4c1"
    ],
    [
      "Map16.sel16",
      1,
      1,
      0,
      [ "@query", "primitive_Prims.op_LessThan" ],
      0,
      "a0d323e2d7fc5a4351ecd234d0e0c81e"
    ],
    [
      "Map16.upd2",
      1,
      1,
      0,
      [ "@query", "primitive_Prims.op_LessThan" ],
      0,
      "27f4d60b610e1631ea84abdc5dec75ec"
    ],
    [
      "Map16.upd4",
      1,
      1,
      0,
      [ "@query", "primitive_Prims.op_LessThan" ],
      0,
      "b22fdd286314ce01f4685b2cde8fcc28"
    ],
    [
      "Map16.upd8",
      1,
      1,
      0,
      [ "@query", "primitive_Prims.op_LessThan" ],
      0,
      "7d97ccaae5e2277bd39a13114a8fd334"
    ],
    [
      "Map16.upd16",
      1,
      1,
      0,
      [ "@query", "primitive_Prims.op_LessThan" ],
      0,
      "0e3391cb75b1686051dce5542710e2bc"
    ],
    [
      "Map16.lemma_self16",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
        "equation_Map16.map16", "equation_Map16.map2", "equation_Map16.map4",
        "equation_Map16.map8", "equation_Map16.sel16", "equation_Map16.sel2",
        "equation_Map16.sel4", "equation_Map16.sel8", "equation_Map16.upd16",
        "equation_Map16.upd2", "equation_Map16.upd4", "equation_Map16.upd8",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "int_inversion", "primitive_Prims.op_LessThan",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "typing_Map16.upd16"
      ],
      0,
      "658c02e39e11544f30f3ac8bbdea17c2"
    ],
    [
      "Map16.lemma_other16",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Map16.map2",
        "equation_Map16.map4", "equation_Map16.map8", "equation_Map16.sel16",
        "equation_Map16.sel2", "equation_Map16.sel4", "equation_Map16.sel8",
        "equation_Map16.upd16", "equation_Map16.upd2", "equation_Map16.upd4",
        "equation_Map16.upd8", "int_inversion", "int_typing",
        "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"
      ],
      0,
      "8a732f59d9013bd324ae5baabd09dec6"
    ],
    [
      "Map16.lemma_equal16",
      1,
      1,
      5,
      [
        "@MaxIFuel_assumption", "@query",
        "data_elim_FStar.Pervasives.Native.Mktuple2", "equation_Map16.map16",
        "equation_Map16.map2", "equation_Map16.map4", "equation_Map16.map8",
        "equation_Map16.sel16", "equation_Map16.sel2", "equation_Map16.sel4",
        "equation_Map16.sel8", "equation_Words_s.pow2_1",
        "equation_Words_s.pow2_2",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Words_s.pow2_1",
        "function_token_typing_Words_s.pow2_2", "int_typing",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "5e2b5df4efd52eb44ac879ffcfec1a27"
    ],
    [
      "Map16.lemma_self",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "2fefda6546a8409b7664b0acf758465b"
    ],
    [
      "Map16.lemma_other",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "3b31dfb833b3742e0f9d964f39290431"
    ],
    [
      "Map16.lemma_equal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "86be14ff0b1a73597fc97ea3c8e8098f"
    ],
    [
      "Map16.lemma_eta16",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Map16.get",
        "int_inversion"
      ],
      0,
      "9caf80dca92c21342b9bf7c7dfd95adc"
    ],
    [
      "Map16.lemma_eta",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "217ba6e7ce025c2be4b29b3d8ee4ef23"
    ]
  ]
]