[
  "8����ো���FD4i4",
  [
    [
      "Vale.Math.Poly2.Galois.irred_poly",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U1@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466"
      ],
      0,
      "17f07df495409a6329d1c9aa0198bf25"
    ],
    [
      "Vale.Math.Poly2.Galois.lemma_shift_left",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned",
        "fuel_guarded_inversion_Spec.GaloisField.field",
        "lemma_Vale.Math.Poly2.Galois.lemma_to_poly_degree",
        "lemma_Vale.Math.Poly2.lemma_degree_at_least",
        "proj_equation_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Lib.IntTypes.unsigned",
        "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "8e555445a296682cafa1988633184258"
    ],
    [
      "Vale.Math.Poly2.Galois.lemma_shift_right",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned",
        "proj_equation_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Lib.IntTypes.unsigned",
        "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "8c60aa457d9e4cebfbee18c719e606f6"
    ]
  ]
]