[
  "�3\u0010p�\b˟S����#�",
  [
    [
      "Vale.X64.InsLemmas.make_instr_t_args",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_5b8a55910a662c783b1ed3212549410e_0",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "disc_equation_Vale.X64.Instruction_s.IOpEx",
        "disc_equation_Vale.X64.Instruction_s.IOpIm",
        "fuel_guarded_inversion_Prims.list",
        "fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "proj_equation_Prims.Cons_hd", "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_7aac12c24449a22c34d98a0ea8ed4a32",
        "subterm_ordering_Prims.Cons", "typing_Prims.__proj__Cons__item__hd"
      ],
      0,
      "67ed7b295db650f7cbfacbfe238a136f"
    ],
    [
      "Vale.X64.InsLemmas.make_instr_t",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6",
        "binder_x_9480187c8e85713ad9eae72e33c57410_0",
        "data_elim_Prims.Cons",
        "data_typing_intro_Vale.X64.Instruction_s.Out@tok",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "disc_equation_Vale.X64.Instruction_s.IOpEx",
        "disc_equation_Vale.X64.Instruction_s.IOpIm",
        "equation_Vale.X64.Instruction_s.instr_out",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "fuel_guarded_inversion_Prims.list",
        "fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_Prims.Cons_hd", "projection_inverse_BoxBool_proj_0",
        "subterm_ordering_Prims.Cons",
        "typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2"
      ],
      0,
      "2ccc8707b039b714041f1b46f9d700a7"
    ],
    [
      "Vale.X64.InsLemmas.make_instr_args",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "Vale.X64.InsLemmas_interpretation_Tm_arrow_4871688054f7faf8ffeb88d2fe387ed5",
        "binder_x_5b8a55910a662c783b1ed3212549410e_0",
        "constructor_distinct_Prims.Nil",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "disc_equation_Vale.X64.Instruction_s.IOpEx",
        "disc_equation_Vale.X64.Instruction_s.IOpIm",
        "equation_Vale.X64.Instruction_s.arrow",
        "equation_Vale.X64.Instruction_s.instr_operand_t",
        "equation_with_fuel_Vale.X64.InsLemmas.make_instr_t_args.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
        "fuel_guarded_inversion_Prims.list",
        "fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "proj_equation_Prims.Cons_hd", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
        "refinement_interpretation_Tm_refine_7aac12c24449a22c34d98a0ea8ed4a32",
        "subterm_ordering_Prims.Cons", "typing_Prims.__proj__Cons__item__hd",
        "typing_Tm_abs_e682630a535575e1da5f42ea8f39afbd", "unit_typing"
      ],
      0,
      "6ff4159653d53b71458f7640b41e7837"
    ],
    [
      "Vale.X64.InsLemmas.make_instr_outs",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.X64.InsLemmas.make_instr_t.fuel_instrumented",
        "@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.InsLemmas.make_instr_t.fuel_instrumented",
        "@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "@query",
        "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "Vale.X64.InsLemmas_interpretation_Tm_arrow_3d5c379ce3103cb9706c98944b5171f4",
        "Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6",
        "binder_x_5b8a55910a662c783b1ed3212549410e_1",
        "binder_x_9480187c8e85713ad9eae72e33c57410_0",
        "constructor_distinct_Prims.Nil",
        "constructor_distinct_Vale.X64.Instruction_s.IOpEx",
        "data_elim_Prims.Cons",
        "data_typing_intro_Vale.X64.Instruction_s.Out@tok",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "disc_equation_Vale.X64.Instruction_s.IOpEx",
        "disc_equation_Vale.X64.Instruction_s.IOpIm",
        "equation_Vale.X64.Instruction_s.arrow",
        "equation_Vale.X64.Instruction_s.instr_operand_t",
        "equation_Vale.X64.Instruction_s.instr_out",
        "equation_with_fuel_Vale.X64.InsLemmas.make_instr_t.fuel_instrumented",
        "equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "fuel_guarded_inversion_Prims.list",
        "fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
        "kinding_Vale.X64.Instruction_s.instr_operand@tok",
        "kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_Prims.Cons_hd",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
        "subterm_ordering_Prims.Cons",
        "typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2",
        "typing_Tm_abs_9479633f5fb2d9990211f1d2c283caf2"
      ],
      0,
      "1aec49f0fff844ef0597abcd8de4bbd9"
    ]
  ]
]