[
  "�N�+N�����k����Q",
  [
    [
      "Vale.Math.Poly2.power",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "600c86e84c5d7207aec0f2cd95a65959"
    ],
    [
      "Vale.Math.Poly2.lemma_mul_reverse",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "652ad8f163160f76f5919dd6685d2010"
    ]
  ]
]