[
  "{yl`\u0015�A\u0005�4\n6�x�",
  [
    [
      "Vale.Set.remove_between'",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_6d0180d4fcd10237cf0d87dd345d77cc_1",
        "binder_x_7a6d54e0c00a8de2fec939f280a0567c_2",
        "binder_x_e3dc4db8239f49f041127584ba34ace6_0", "bool_inversion",
        "equality_tok_Prims.LexTop@tok",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int", "int_inversion", "int_typing",
        "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
        "lemma_FStar.Set.mem_singleton", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Negation",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_b154ce3b342a495bb8730cab2e6b9e58",
        "refinement_interpretation_Tm_refine_c37f34c764eca44770d9788f05b065d6",
        "typing_FStar.Set.complement", "typing_FStar.Set.mem",
        "typing_FStar.Set.singleton", "well-founded-ordering-on-nat"
      ],
      0,
      "331db8d32b5d0124d5a7f311b2da516c"
    ],
    [
      "Vale.Set.remove_between",
      1,
      1,
      0,
      [ "@query", "primitive_Prims.op_LessThanOrEqual" ],
      0,
      "a2f6d5dedb90fc3a956397bfb188424b"
    ],
    [
      "Vale.Set.remove_between_reveal",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "equation_Vale.Set.remove_between",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int", "int_inversion",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_5d68b4aedab07e9543c96792e76744c9",
        "refinement_interpretation_Tm_refine_dd324af5af82160c4ba8a3d42578b869",
        "typing_FStar.Set.mem", "typing_Vale.Set.remove_between",
        "typing_Vale.Set.remove_between_"
      ],
      0,
      "fc1148b3a649750019f7957adea5ba18"
    ],
    [
      "Vale.Set.lemma_sel_restrict",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.Map.restrict", "equation_FStar.Map.sel",
        "fuel_guarded_inversion_FStar.Map.t",
        "function_token_typing_Prims.__cache_version_number__",
        "proj_equation_FStar.Map.Mkt_mappings",
        "projection_inverse_FStar.Map.Mkt_mappings",
        "token_correspondence_FStar.Map.__proj__Mkt__item__mappings"
      ],
      0,
      "1180de63708d58d1ca6e37c001450891"
    ]
  ]
]