[
  "��j\u0013x]��3\u001dsx���.",
  [
    [
      "CanonCommSwaps.apply_swap_aux",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.List.Tot.Base.length"
      ],
      0,
      "519190a1ec541573154a671dc074a3f0"
    ],
    [
      "CanonCommSwaps.apply_swap_aux",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_0a56e3de562c08d8ab59f4ac6f626a98_3",
        "binder_x_51061ea2dc38a177fafabb4a7c352156_4",
        "binder_x_e22ba7a032a73f6d0678d3d186686631_2",
        "binder_x_fe28d8bcde588226b4e538b35321de05_1",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "data_elim_Prims.Cons", "data_typing_intro_Prims.Cons@tok",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "equality_tok_Prims.LexTop@tok", "equation_CanonCommSwaps.swap",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "fuel_guarded_inversion_Prims.list",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
        "proj_equation_Prims.Cons_tl", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "refinement_interpretation_Tm_refine_1a90870aa2e2cdbf55c12113e539b1bc",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "subterm_ordering_Prims.Cons"
      ],
      0,
      "7061d3c07a66f5d544019b39d1422328"
    ],
    [
      "CanonCommSwaps.apply_swaps",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "binder_x_0a56e3de562c08d8ab59f4ac6f626a98_2",
        "binder_x_6c7967d2906cfab79d4a5df841447e1d_3",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "equality_tok_Prims.LexTop@tok", "equation_CanonCommSwaps.swap",
        "equation_Prims.nat", "fuel_guarded_inversion_Prims.list",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_tl",
        "refinement_interpretation_CanonCommSwaps_Tm_refine_1a90870aa2e2cdbf55c12113e539b1bc",
        "subterm_ordering_Prims.Cons"
      ],
      0,
      "3657795fc6306757ba16b28054db05a8"
    ],
    [
      "CanonCommSwaps.extend_equal_counts",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.count.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.count.fuel_instrumented",
        "@query", "constructor_distinct_Prims.Cons",
        "data_typing_intro_Prims.Cons@tok",
        "equation_CanonCommSwaps.equal_counts", "equation_Prims.eqtype",
        "equation_with_fuel_FStar.List.Tot.Base.count.fuel_instrumented",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "a6f29a12a12e6c3cca1ad8f36e64203c"
    ],
    [
      "CanonCommSwaps.retract_equal_counts",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.count.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.count.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Prims.Cons", "data_elim_Prims.Cons",
        "data_typing_intro_Prims.Cons@tok",
        "equation_CanonCommSwaps.equal_counts", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.count.fuel_instrumented",
        "fuel_guarded_inversion_Prims.list",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "token_correspondence_FStar.List.Tot.Base.count.fuel_instrumented",
        "typing_FStar.List.Tot.Base.count"
      ],
      0,
      "dc0c44e5cec48823501a2a31a5cf9e4b"
    ],
    [
      "CanonCommSwaps.append_swaps",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "789385811cac5ed535ff666cd1f24231"
    ],
    [
      "CanonCommSwaps.append_swaps",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_CanonCommSwaps.apply_swaps.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_CanonCommSwaps.apply_swaps.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.append.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_134152e07c968ca4284eca3b9d9489d3_2",
        "binder_x_134152e07c968ca4284eca3b9d9489d3_3",
        "binder_x_273c0cb114efbc10b99731f088b17ae0_0",
        "binder_x_a7fb6faea5d851896150f3c74abbb25a_1",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "equality_tok_Prims.LexTop@tok", "equation_CanonCommSwaps.swap",
        "equation_FStar.List.Tot.Base.op_At", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_with_fuel_CanonCommSwaps.apply_swaps.fuel_instrumented",
        "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "fuel_guarded_inversion_Prims.list",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "refinement_interpretation_Tm_refine_1a90870aa2e2cdbf55c12113e539b1bc",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "subterm_ordering_Prims.Cons", "typing_CanonCommSwaps.swap",
        "typing_FStar.List.Tot.Base.length",
        "typing_FStar.List.Tot.Base.op_At"
      ],
      0,
      "e65994c2a9de83e3ed9aee22117fa284"
    ],
    [
      "CanonCommSwaps.lift_swap_cons",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "constructor_distinct_Prims.Cons",
        "data_typing_intro_Prims.Cons@tok", "equation_CanonCommSwaps.swap",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Prims.squash",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "refinement_interpretation_Tm_refine_0463eac50fad03cb37dea5b73a604cd0",
        "refinement_interpretation_Tm_refine_1a90870aa2e2cdbf55c12113e539b1bc",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.List.Tot.Base.length", "unit_typing"
      ],
      0,
      "9a505183ee0f1d1d77ff5fe768331e7e"
    ],
    [
      "CanonCommSwaps.lift_swap_cons",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_CanonCommSwaps.apply_swap_aux.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_CanonCommSwaps.apply_swap_aux.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_3862c4e8ff39bfc3871b6a47e7ff5b2e",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "binder_x_273c0cb114efbc10b99731f088b17ae0_0",
        "binder_x_9ab5a2235d8a84d0dee72b1726e27096_4",
        "binder_x_a7fb6faea5d851896150f3c74abbb25a_3",
        "binder_x_e22ba7a032a73f6d0678d3d186686631_1",
        "binder_x_f5f822c6aa182796e6c581814ec64033_2",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "constructor_distinct_Prims.list", "constructor_distinct_Prims.unit",
        "constructor_distinct_Tm_unit", "data_elim_Prims.Cons",
        "data_typing_intro_Prims.Cons@tok", "disc_equation_Prims.Cons",
        "disc_equation_Prims.Nil", "equality_tok_Prims.LexTop@tok",
        "equation_CanonCommSwaps.swap", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_with_fuel_CanonCommSwaps.apply_swap_aux.fuel_instrumented",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "fuel_guarded_inversion_Prims.list",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "refinement_interpretation_Tm_refine_090a06f8cdcdd6c3a2b22a117754681d",
        "refinement_interpretation_Tm_refine_1a90870aa2e2cdbf55c12113e539b1bc",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "subterm_ordering_Prims.Cons",
        "typing_CanonCommSwaps.apply_swap_aux",
        "typing_FStar.List.Tot.Base.length", "unit_inversion", "unit_typing"
      ],
      0,
      "d261ca6a982635b28879cd6a8dce2cfd"
    ],
    [
      "CanonCommSwaps.lift_swaps_cons",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_CanonCommSwaps.apply_swaps.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_CanonCommSwaps.apply_swaps.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_273c0cb114efbc10b99731f088b17ae0_0",
        "binder_x_6132f4352d070b0f907e3833569ceb26_3",
        "binder_x_a7fb6faea5d851896150f3c74abbb25a_2",
        "binder_x_f5f822c6aa182796e6c581814ec64033_1",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "data_typing_intro_Prims.Cons@tok", "disc_equation_Prims.Cons",
        "disc_equation_Prims.Nil", "equality_tok_Prims.LexTop@tok",
        "equation_CanonCommSwaps.apply_swap", "equation_CanonCommSwaps.swap",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_with_fuel_CanonCommSwaps.apply_swaps.fuel_instrumented",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "fuel_guarded_inversion_Prims.list",
        "function_token_typing_CanonCommSwaps.apply_swap_aux",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "refinement_interpretation_Tm_refine_1a90870aa2e2cdbf55c12113e539b1bc",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "subterm_ordering_Prims.Cons",
        "token_correspondence_CanonCommSwaps.apply_swap"
      ],
      0,
      "3a0d199916cae4c49bc6ce443930fe5a"
    ],
    [
      "CanonCommSwaps.swap_to_front",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "148eec9ce7deb910c4e9d0931f58906f"
    ],
    [
      "CanonCommSwaps.swap_to_front",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_CanonCommSwaps.apply_swap_aux.fuel_instrumented",
        "@fuel_correspondence_CanonCommSwaps.apply_swaps.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.count.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.count.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query",
        "CanonCommSwaps_interpretation_Tm_arrow_7b5f1f59a8320af71c1af73e702c987e",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_273c0cb114efbc10b99731f088b17ae0_0",
        "binder_x_a7fb6faea5d851896150f3c74abbb25a_2",
        "binder_x_f5f822c6aa182796e6c581814ec64033_1",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "data_elim_Prims.Cons", "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok", "disc_equation_Prims.Cons",
        "equality_tok_Prims.LexTop@tok",
        "equation_CanonCommSwaps.apply_swap",
        "equation_CanonCommSwaps.equal_counts",
        "equation_CanonCommSwaps.swap", "equation_FStar.List.Tot.Base.hd",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_with_fuel_CanonCommSwaps.apply_swap_aux.fuel_instrumented",
        "equation_with_fuel_CanonCommSwaps.apply_swaps.fuel_instrumented",
        "equation_with_fuel_FStar.List.Tot.Base.count.fuel_instrumented",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "fuel_guarded_inversion_Prims.list",
        "function_token_typing_CanonCommSwaps.apply_swap_aux",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "refinement_interpretation_Tm_refine_090a06f8cdcdd6c3a2b22a117754681d",
        "refinement_interpretation_Tm_refine_1a90870aa2e2cdbf55c12113e539b1bc",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "subterm_ordering_Prims.Cons",
        "token_correspondence_CanonCommSwaps.apply_swap",
        "token_correspondence_CanonCommSwaps.apply_swap_aux",
        "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "typing_CanonCommSwaps.apply_swaps", "typing_CanonCommSwaps.swap",
        "typing_FStar.List.Tot.Base.length"
      ],
      0,
      "398ab04c74cdcc9cb55bf78f4381f3e5"
    ],
    [
      "CanonCommSwaps.equal_counts_implies_swaps",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_CanonCommSwaps.apply_swaps.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.count.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.count.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_273c0cb114efbc10b99731f088b17ae0_0",
        "binder_x_a7fb6faea5d851896150f3c74abbb25a_1",
        "binder_x_a7fb6faea5d851896150f3c74abbb25a_2",
        "constructor_distinct_Prims.Nil", "disc_equation_Prims.Cons",
        "disc_equation_Prims.Nil", "equality_tok_Prims.LexTop@tok",
        "equation_CanonCommSwaps.equal_counts",
        "equation_CanonCommSwaps.swap", "equation_FStar.List.Tot.Base.hd",
        "equation_FStar.List.Tot.Base.tail",
        "equation_FStar.List.Tot.Base.tl", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_with_fuel_CanonCommSwaps.apply_swaps.fuel_instrumented",
        "equation_with_fuel_FStar.List.Tot.Base.count.fuel_instrumented",
        "fuel_guarded_inversion_Prims.list",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "subterm_ordering_Prims.Cons",
        "token_correspondence_FStar.List.Tot.Base.count.fuel_instrumented"
      ],
      0,
      "0ad48382dd3e0d6f86f70fce65ecc0ed"
    ]
  ]
]