∀ (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (ringInst semiringInst : Lean.Expr) (charInst? : Option (Lean.Expr × ℕ))
  (addFn? mulFn? subFn? negFn? powFn? intCastFn? natCastFn? one? : Option Lean.Expr) (vars : Lean.PArray Lean.Expr)
  (varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var)
  (denote : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.RingExpr) (id_1 : ℕ) (type_1 : Lean.Expr)
  (u_1 : Lean.Level) (ringInst_1 semiringInst_1 : Lean.Expr) (charInst?_1 : Option (Lean.Expr × ℕ))
  (addFn?_1 mulFn?_1 subFn?_1 negFn?_1 powFn?_1 intCastFn?_1 natCastFn?_1 one?_1 : Option Lean.Expr)
  (vars_1 : Lean.PArray Lean.Expr) (varMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var)
  (denote_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.RingExpr),
  ({ id := id, type := type, u := u, ringInst := ringInst, semiringInst := semiringInst, charInst? := charInst?,
        addFn? := addFn?, mulFn? := mulFn?, subFn? := subFn?, negFn? := negFn?, powFn? := powFn?,
        intCastFn? := intCastFn?, natCastFn? := natCastFn?, one? := one?, vars := vars, varMap := varMap,
        denote := denote } =
      { id := id_1, type := type_1, u := u_1, ringInst := ringInst_1, semiringInst := semiringInst_1,
        charInst? := charInst?_1, addFn? := addFn?_1, mulFn? := mulFn?_1, subFn? := subFn?_1, negFn? := negFn?_1,
        powFn? := powFn?_1, intCastFn? := intCastFn?_1, natCastFn? := natCastFn?_1, one? := one?_1, vars := vars_1,
        varMap := varMap_1, denote := denote_1 }) =
    (id = id_1 ∧
      type = type_1 ∧
        u = u_1 ∧
          ringInst = ringInst_1 ∧
            semiringInst = semiringInst_1 ∧
              charInst? = charInst?_1 ∧
                addFn? = addFn?_1 ∧
                  mulFn? = mulFn?_1 ∧
                    subFn? = subFn?_1 ∧
                      negFn? = negFn?_1 ∧
                        powFn? = powFn?_1 ∧
                          intCastFn? = intCastFn?_1 ∧
                            natCastFn? = natCastFn?_1 ∧
                              one? = one?_1 ∧ vars = vars_1 ∧ varMap = varMap_1 ∧ denote = denote_1)