[
  "�z�ZZ��2\u000e:���鰙",
  [
    [
      "Meta.Interface.assoc",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.assoc.fuel_instrumented",
        "@query", "bool_inversion",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "equation_with_fuel_FStar.List.Tot.Base.assoc.fuel_instrumented",
        "lemma_FStar.Pervasives.invertOption",
        "projection_inverse_BoxBool_proj_0",
        "typing_FStar.List.Tot.Base.assoc",
        "typing_FStar.Pervasives.Native.uu___is_Some"
      ],
      0,
      "7d3b977b52082f83aa23f4f517830996"
    ],
    [
      "Meta.Interface.__proj__Inline__item__new_name",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Meta.Interface.Inline",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_72d871bdf0e6e15cb9b70b8f1ef82b10"
      ],
      0,
      "12223cf188c49f4361b91e5ba98317dc"
    ],
    [
      "Meta.Interface.string_of_mapping",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Meta.Interface.Inline",
        "disc_equation_Meta.Interface.Specialize",
        "fuel_guarded_inversion_Meta.Interface.mapping"
      ],
      0,
      "cfc7779a752939e694fb809523651417"
    ],
    [
      "Meta.Interface.string_of_name",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_Prims.Cons",
        "disc_equation_Prims.Nil", "equation_FStar.Reflection.Types.name",
        "fuel_guarded_inversion_Prims.list"
      ],
      0,
      "91e7d39956bf12c852ad952232f8a3c1"
    ],
    [
      "Meta.Interface.suffix_name",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_Prims.Cons",
        "disc_equation_Prims.Nil", "equation_FStar.Reflection.Types.name",
        "fuel_guarded_inversion_Prims.list"
      ],
      0,
      "90dfdce509766efa0ca10845230b914c"
    ],
    [
      "Meta.Interface.in_namespace",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_20ccd379c93014ff7fe3312d7f024a43_0",
        "binder_x_dce109b66917edb1ca83b9408101b740_1",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "equation_FStar.Reflection.Types.name",
        "fuel_guarded_inversion_Prims.list",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "subterm_ordering_Prims.Cons"
      ],
      0,
      "73765e2b28a72e3a91406fcc415d3a9c"
    ],
    [
      "Meta.Interface.must",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "lemma_FStar.Pervasives.invertOption",
        "projection_inverse_BoxBool_proj_0",
        "typing_FStar.Pervasives.Native.uu___is_Some"
      ],
      0,
      "261e78abdb536e500bf58f06bf2f95c1"
    ],
    [
      "Meta.Interface.visit_function",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_FStar.Tactics.Result.Failed",
        "constructor_distinct_FStar.Tactics.Result.Success",
        "disc_equation_FStar.Pervasives.Native.None",
        "fuel_guarded_inversion_FStar.Tactics.Result.__result",
        "function_token_typing_FStar.Reflection.Types.sigelt",
        "lemma_FStar.Pervasives.invertOption",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Tactics.Result.Failed_a",
        "projection_inverse_FStar.Tactics.Result.Failed_exn",
        "projection_inverse_FStar.Tactics.Result.Failed_ps",
        "projection_inverse_FStar.Tactics.Result.Success_a",
        "projection_inverse_FStar.Tactics.Result.Success_ps",
        "projection_inverse_FStar.Tactics.Result.Success_v",
        "typing_FStar.Pervasives.Native.uu___is_Some"
      ],
      0,
      "8aeb537584922f88abe2bc59bfc8d8f2"
    ],
    [
      "Meta.Interface.visit_function",
      2,
      2,
      2,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.assoc.fuel_instrumented",
        "@query",
        "FStar.Reflection.Data_pretyping_ee655bc751cef679bca813f86c407d6b",
        "Meta.Interface_pretyping_3687ebf883f49bee7aa0812c87d03fff",
        "Prims_pretyping_ce036b6b736ef4e0bc3a9ff132a12aed",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "bool_typing", "constructor_distinct_FStar.Tactics.Result.Failed",
        "constructor_distinct_FStar.Tactics.Result.Success",
        "constructor_distinct_Meta.Interface.Specialize",
        "data_elim_FStar.Tactics.Result.Success",
        "data_elim_Meta.Interface.Mkstate",
        "data_typing_intro_FStar.Reflection.Data.Tv_Unknown@tok",
        "data_typing_intro_Meta.Interface.Specialize@tok",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "disc_equation_FStar.Reflection.Data.Tv_Abs",
        "disc_equation_FStar.Reflection.Data.Tv_App",
        "disc_equation_FStar.Reflection.Data.Tv_Arrow",
        "disc_equation_FStar.Reflection.Data.Tv_AscribedC",
        "disc_equation_FStar.Reflection.Data.Tv_AscribedT",
        "disc_equation_FStar.Reflection.Data.Tv_BVar",
        "disc_equation_FStar.Reflection.Data.Tv_Const",
        "disc_equation_FStar.Reflection.Data.Tv_FVar",
        "disc_equation_FStar.Reflection.Data.Tv_Let",
        "disc_equation_FStar.Reflection.Data.Tv_Match",
        "disc_equation_FStar.Reflection.Data.Tv_Refine",
        "disc_equation_FStar.Reflection.Data.Tv_Type",
        "disc_equation_FStar.Reflection.Data.Tv_Unknown",
        "disc_equation_FStar.Reflection.Data.Tv_Uvar",
        "disc_equation_FStar.Reflection.Data.Tv_Var",
        "disc_equation_Meta.Interface.Inline",
        "disc_equation_Meta.Interface.Specialize",
        "equation_FStar.Reflection.Data.argv",
        "equation_FStar.Reflection.Types.name", "equation_Prims.eqtype",
        "fuel_guarded_inversion_FStar.Reflection.Data.term_view",
        "fuel_guarded_inversion_FStar.Tactics.Result.__result",
        "fuel_guarded_inversion_Meta.Interface.mapping",
        "fuel_guarded_inversion_Meta.Interface.state",
        "fuel_guarded_inversion_Prims.list",
        "function_token_typing_FStar.Reflection.Types.bv",
        "function_token_typing_FStar.Reflection.Types.term",
        "function_token_typing_Prims.bool",
        "function_token_typing_Prims.string",
        "kinding_FStar.Pervasives.Native.tuple4@tok",
        "kinding_Meta.Interface.mapping@tok", "kinding_Prims.list@tok",
        "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Negation",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Tactics.Result.Failed_a",
        "projection_inverse_FStar.Tactics.Result.Failed_exn",
        "projection_inverse_FStar.Tactics.Result.Failed_ps",
        "projection_inverse_FStar.Tactics.Result.Success_a",
        "projection_inverse_FStar.Tactics.Result.Success_ps",
        "projection_inverse_FStar.Tactics.Result.Success_v",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_FStar.List.Tot.Base.assoc",
        "typing_FStar.Pervasives.Native.uu___is_None",
        "typing_FStar.Reflection.Basic.inspect_fv",
        "typing_FStar.Reflection.Types.name",
        "typing_Meta.Interface.__proj__Mkstate__item__seen", "unit_typing"
      ],
      0,
      "c2df2e3dcff0bb978183c09fc60c910f"
    ]
  ]
]