[
  "Î\u000f\u001eËç\u0014Ä\u00061U\u001dšêð.ö",
  [
    [
      "Vale.Math.Poly2.Galois.Lemmas.lemma_eq_to_poly",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "48255034fdd3406a84430ce95764db55"
    ],
    [
      "Vale.Math.Poly2.Galois.Lemmas.lemma_mul_zero",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_Spec.GaloisField.field",
        "function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
        "lemma_Vale.Math.Poly2.Galois.lemma_irred_degree",
        "lemma_Vale.Math.Poly2.Galois.lemma_mul",
        "lemma_Vale.Math.Poly2.Galois.lemma_to_poly_degree",
        "lemma_Vale.Math.Poly2.Galois.lemma_zero",
        "lemma_Vale.Math.Poly2.lemma_degree_at_least",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303",
        "typing_Spec.GaloisField.zero",
        "typing_Vale.Math.Poly2.Galois.to_poly"
      ],
      0,
      "27d540c022b52c207326fb4bc149aaae"
    ],
    [
      "Vale.Math.Poly2.Galois.Lemmas.lemma_mul_one",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_Spec.GaloisField.field",
        "lemma_Vale.Math.Poly2.Galois.lemma_irred_degree",
        "lemma_Vale.Math.Poly2.Galois.lemma_mul",
        "lemma_Vale.Math.Poly2.Galois.lemma_one",
        "lemma_Vale.Math.Poly2.Galois.lemma_to_poly_degree",
        "lemma_Vale.Math.Poly2.lemma_degree_at_least",
        "typing_Spec.GaloisField.one",
        "typing_Vale.Math.Poly2.Galois.to_poly"
      ],
      0,
      "90a04da6178dcc843bb0d3d6c97ff46a"
    ],
    [
      "Vale.Math.Poly2.Galois.Lemmas.lemma_mul_commute",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_Spec.GaloisField.field",
        "lemma_Vale.Math.Poly2.Galois.lemma_mul"
      ],
      0,
      "f9540856f38871d8362441eb28f21106"
    ],
    [
      "Vale.Math.Poly2.Galois.Lemmas.lemma_mul_associate",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_Spec.GaloisField.field",
        "lemma_Vale.Math.Poly2.Galois.lemma_irred_degree",
        "lemma_Vale.Math.Poly2.Galois.lemma_mul",
        "lemma_Vale.Math.Poly2.Galois.lemma_to_poly_degree",
        "lemma_Vale.Math.Poly2.lemma_degree_at_least",
        "typing_Spec.GaloisField.fmul",
        "typing_Vale.Math.Poly2.Galois.to_poly"
      ],
      0,
      "eead771f771906e0dc328505bb545020"
    ],
    [
      "Vale.Math.Poly2.Galois.Lemmas.lemma_mul_distribute_left",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_Spec.GaloisField.field",
        "lemma_Vale.Math.Poly2.Galois.lemma_add",
        "lemma_Vale.Math.Poly2.Galois.lemma_irred_degree",
        "lemma_Vale.Math.Poly2.Galois.lemma_mul",
        "lemma_Vale.Math.Poly2.Galois.lemma_to_poly_degree",
        "lemma_Vale.Math.Poly2.lemma_degree_at_least",
        "typing_Spec.GaloisField.fadd", "typing_Spec.GaloisField.fmul",
        "typing_Vale.Math.Poly2.Galois.to_poly"
      ],
      0,
      "250ec519a276b4a775da6f542d1ee25c"
    ],
    [
      "Vale.Math.Poly2.Galois.Lemmas.lemma_mul_distribute_right",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "e6ee7b5d524f8fbc7be2bfefa3b5af8d"
    ]
  ]
]