∀ (rings : Array Lean.Meta.Grind.Arith.CommRing.CommRing) (typeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (exprToRingId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ) (semirings : Array Lean.Meta.Grind.Arith.CommRing.CommSemiring)
  (stypeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (exprToSemiringId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ) (ncRings : Array Lean.Meta.Grind.Arith.CommRing.Ring)
  (exprToNCRingId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ) (nctypeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (ncSemirings : Array Lean.Meta.Grind.Arith.CommRing.Semiring)
  (exprToNCSemiringId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ)
  (ncstypeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)) (steps : ℕ)
  (rings_1 : Array Lean.Meta.Grind.Arith.CommRing.CommRing)
  (typeIdOf_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)) (exprToRingId_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ)
  (semirings_1 : Array Lean.Meta.Grind.Arith.CommRing.CommSemiring)
  (stypeIdOf_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (exprToSemiringId_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ) (ncRings_1 : Array Lean.Meta.Grind.Arith.CommRing.Ring)
  (exprToNCRingId_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ)
  (nctypeIdOf_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (ncSemirings_1 : Array Lean.Meta.Grind.Arith.CommRing.Semiring)
  (exprToNCSemiringId_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ)
  (ncstypeIdOf_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)) (steps_1 : ℕ),
  ({ rings := rings, typeIdOf := typeIdOf, exprToRingId := exprToRingId, semirings := semirings, stypeIdOf := stypeIdOf,
        exprToSemiringId := exprToSemiringId, ncRings := ncRings, exprToNCRingId := exprToNCRingId,
        nctypeIdOf := nctypeIdOf, ncSemirings := ncSemirings, exprToNCSemiringId := exprToNCSemiringId,
        ncstypeIdOf := ncstypeIdOf, steps := steps } =
      { rings := rings_1, typeIdOf := typeIdOf_1, exprToRingId := exprToRingId_1, semirings := semirings_1,
        stypeIdOf := stypeIdOf_1, exprToSemiringId := exprToSemiringId_1, ncRings := ncRings_1,
        exprToNCRingId := exprToNCRingId_1, nctypeIdOf := nctypeIdOf_1, ncSemirings := ncSemirings_1,
        exprToNCSemiringId := exprToNCSemiringId_1, ncstypeIdOf := ncstypeIdOf_1, steps := steps_1 }) =
    (rings = rings_1 ∧
      typeIdOf = typeIdOf_1 ∧
        exprToRingId = exprToRingId_1 ∧
          semirings = semirings_1 ∧
            stypeIdOf = stypeIdOf_1 ∧
              exprToSemiringId = exprToSemiringId_1 ∧
                ncRings = ncRings_1 ∧
                  exprToNCRingId = exprToNCRingId_1 ∧
                    nctypeIdOf = nctypeIdOf_1 ∧
                      ncSemirings = ncSemirings_1 ∧
                        exprToNCSemiringId = exprToNCSemiringId_1 ∧ ncstypeIdOf = ncstypeIdOf_1 ∧ steps = steps_1)