[
  "\u0001\u001e~�AI�\u0016�H�\u000b\u0011df�",
  [
    [
      "Words.Two_s.nat_to_two_unfold",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "a3b3f330b197b55d96e4d2b2243edce7"
    ],
    [
      "Words.Two_s.nat_to_two_unfold",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
      ],
      0,
      "f4a6220fda2b633bda1e5f39c606e176"
    ],
    [
      "Words.Two_s.nat_to_two",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "d5ba7dcb242b049a9697af43843b89ba"
    ],
    [
      "Words.Two_s.nat_to_two",
      2,
      1,
      0,
      [ "@query" ],
      0,
      "f8eeeda2ba1f3618a2a58eb86c308351"
    ],
    [
      "Words.Two_s.two_to_nat_unfold",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "4a235d888a27377a83c2010979f0fffc"
    ],
    [
      "Words.Two_s.two_to_nat_unfold",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
      ],
      0,
      "a638fc3400ac212d86bab9c87cd5b8f7"
    ],
    [
      "Words.Two_s.two_to_nat",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "708ccccf2ef90c831c81f0f0bc77ba7a"
    ],
    [
      "Words.Two_s.two_to_nat",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "4844030f6891a50bb9fc6c86841abfcf"
    ],
    [
      "Words.Two_s.two_select",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Words_s.nat1",
        "equation_Words_s.natN",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "cd49491d2b0b33b9c2ca280a57a6c7f8"
    ],
    [
      "Words.Two_s.two_insert",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Words_s.nat1",
        "equation_Words_s.natN",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "5f05306a93b671d7039e1dd1c42ba664"
    ]
  ]
]