∀ {vars : Lean.PArray Lean.Expr} {varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Linear.Var}
  {vars' : Lean.PArray Lean.Expr} {varMap' : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Linear.Var}
  {natToIntMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr)}
  {natDef : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Linear.Var}
  {dvds : Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr)}
  {lowers uppers : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.LeCnstr)}
  {diseqs : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr)}
  {elimEqs : Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr)} {elimStack : List Int.Linear.Var}
  {occurs : Lean.PArray Lean.Meta.Grind.Arith.Cutsat.VarSet} {assignment : Lean.PArray ℚ} {nextCnstrId : ℕ}
  {caseSplits : Bool} {conflict? : Option Lean.Meta.Grind.Arith.Cutsat.UnsatProof}
  {diseqSplits : Lean.PHashMap Int.Linear.Poly Lean.FVarId} {divMod : Lean.PHashSet (Lean.Expr × ℤ)}
  {toIntIds : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {toIntInfos : Lean.PArray Lean.Meta.Grind.Arith.Cutsat.ToIntInfo}
  {toIntTermMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo}
  {toIntVarMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr} {usedCommRing : Bool}
  {nonlinearOccs : Lean.PHashMap Int.Linear.Var (List Int.Linear.Var)} {vars_1 : Lean.PArray Lean.Expr}
  {varMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Linear.Var} {vars'_1 : Lean.PArray Lean.Expr}
  {varMap'_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Linear.Var}
  {natToIntMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr)}
  {natDef_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Linear.Var}
  {dvds_1 : Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr)}
  {lowers_1 uppers_1 : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.LeCnstr)}
  {diseqs_1 : Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr)}
  {elimEqs_1 : Lean.PArray (Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr)} {elimStack_1 : List Int.Linear.Var}
  {occurs_1 : Lean.PArray Lean.Meta.Grind.Arith.Cutsat.VarSet} {assignment_1 : Lean.PArray ℚ} {nextCnstrId_1 : ℕ}
  {caseSplits_1 : Bool} {conflict?_1 : Option Lean.Meta.Grind.Arith.Cutsat.UnsatProof}
  {diseqSplits_1 : Lean.PHashMap Int.Linear.Poly Lean.FVarId} {divMod_1 : Lean.PHashSet (Lean.Expr × ℤ)}
  {toIntIds_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)}
  {toIntInfos_1 : Lean.PArray Lean.Meta.Grind.Arith.Cutsat.ToIntInfo}
  {toIntTermMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo}
  {toIntVarMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr} {usedCommRing_1 : Bool}
  {nonlinearOccs_1 : Lean.PHashMap Int.Linear.Var (List Int.Linear.Var)},
  { vars := vars, varMap := varMap, vars' := vars', varMap' := varMap', natToIntMap := natToIntMap, natDef := natDef,
        dvds := dvds, lowers := lowers, uppers := uppers, diseqs := diseqs, elimEqs := elimEqs, elimStack := elimStack,
        occurs := occurs, assignment := assignment, nextCnstrId := nextCnstrId, caseSplits := caseSplits,
        conflict? := conflict?, diseqSplits := diseqSplits, divMod := divMod, toIntIds := toIntIds,
        toIntInfos := toIntInfos, toIntTermMap := toIntTermMap, toIntVarMap := toIntVarMap,
        usedCommRing := usedCommRing, nonlinearOccs := nonlinearOccs } =
      { vars := vars_1, varMap := varMap_1, vars' := vars'_1, varMap' := varMap'_1, natToIntMap := natToIntMap_1,
        natDef := natDef_1, dvds := dvds_1, lowers := lowers_1, uppers := uppers_1, diseqs := diseqs_1,
        elimEqs := elimEqs_1, elimStack := elimStack_1, occurs := occurs_1, assignment := assignment_1,
        nextCnstrId := nextCnstrId_1, caseSplits := caseSplits_1, conflict? := conflict?_1,
        diseqSplits := diseqSplits_1, divMod := divMod_1, toIntIds := toIntIds_1, toIntInfos := toIntInfos_1,
        toIntTermMap := toIntTermMap_1, toIntVarMap := toIntVarMap_1, usedCommRing := usedCommRing_1,
        nonlinearOccs := nonlinearOccs_1 } →
    vars = vars_1 ∧ varMap = varMap_1 ∧ ⋯