[
  "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,
      "bb23b05e7efa1a001de750e858a1244d"
    ],
    [
      "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,
      "eec5a2f584eddff9d9449c062c099933"
    ],
    [
      "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,
      "fa71dde435184af73a7305b2b27d0a41"
    ]
  ]
]