[
  "_v�Ɲ�+˺υ��e�",
  [
    [
      "Vale.Lib.Set.remove_between'",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_ae567c2fb75be05905677af440075565_1",
        "binder_x_d7225297ca1a1ec6844d3652f1a46890_2",
        "binder_x_d81ce3e0a7e9266eb475a56ef4ca0603_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_6268074eed4ab807d2471ecaa6d94df2",
        "refinement_interpretation_Tm_refine_a1de8daedb3a03e65182911e08473885",
        "typing_FStar.Set.complement", "typing_FStar.Set.mem",
        "typing_FStar.Set.singleton", "well-founded-ordering-on-nat"
      ],
      0,
      "2f6d22242ba956500dd20e74ada84b80"
    ],
    [
      "Vale.Lib.Set.remove_between",
      1,
      1,
      0,
      [ "@query", "primitive_Prims.op_LessThanOrEqual" ],
      0,
      "03c21c15ee2753f91408ff5fe6541ed6"
    ],
    [
      "Vale.Lib.Set.remove_between_reveal",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "equation_Vale.Lib.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_72ffcbdb7a7dbf1acd542d96c7babf51",
        "refinement_interpretation_Tm_refine_73f213e2db1ed36fbfb9c962fdf7a80a",
        "typing_FStar.Set.mem", "typing_Vale.Lib.Set.remove_between",
        "typing_Vale.Lib.Set.remove_between_"
      ],
      0,
      "a967fab019a25b1a7c920cd92410bb82"
    ],
    [
      "Vale.Lib.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,
      "06df4e4631fa6201b04a3f2d73cfa977"
    ]
  ]
]