{P : Sort u} →
  {id : ℕ} →
    {type : Lean.Expr} →
      {u : Lean.Level} →
        {isPreorderInst leInst : Lean.Expr} →
          {ltInst? isPartialInst? isLinearPreInst? lawfulOrderLTInst? : Option Lean.Expr} →
            {ringId? : Option ℕ} →
              {isCommRing : Bool} →
                {ringInst? orderedRingInst? : Option Lean.Expr} →
                  {leFn : Lean.Expr} →
                    {ltFn? : Option Lean.Expr} →
                      {nodes : Lean.PArray Lean.Expr} →
                        {nodeMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Order.NodeId} →
                          {cnstrs :
                              Lean.PHashMap Lean.Meta.Sym.ExprPtr
                                (Lean.Meta.Grind.Order.Cnstr Lean.Meta.Grind.Order.NodeId)} →
                            {cnstrsOf :
                                Lean.PHashMap (Lean.Meta.Grind.Order.NodeId × Lean.Meta.Grind.Order.NodeId)
                                  (List (Lean.Meta.Grind.Order.Cnstr Lean.Meta.Grind.Order.NodeId × Lean.Expr))} →
                              {sources targets :
                                  Lean.PArray
                                    (Lean.AssocList Lean.Meta.Grind.Order.NodeId Lean.Meta.Grind.Order.Weight)} →
                                {proofs :
                                    Lean.PArray
                                      (Lean.AssocList Lean.Meta.Grind.Order.NodeId Lean.Meta.Grind.Order.ProofInfo)} →
                                  {propagate : List Lean.Meta.Grind.Order.ToPropagate} →
                                    {id' : ℕ} →
                                      {type' : Lean.Expr} →
                                        {u' : Lean.Level} →
                                          {isPreorderInst' leInst' : Lean.Expr} →
                                            {ltInst?' isPartialInst?' isLinearPreInst?' lawfulOrderLTInst?' :
                                                Option Lean.Expr} →
                                              {ringId?' : Option ℕ} →
                                                {isCommRing' : Bool} →
                                                  {ringInst?' orderedRingInst?' : Option Lean.Expr} →
                                                    {leFn' : Lean.Expr} →
                                                      {ltFn?' : Option Lean.Expr} →
                                                        {nodes' : Lean.PArray Lean.Expr} →
                                                          {nodeMap' :
                                                              Lean.PHashMap Lean.Meta.Sym.ExprPtr
                                                                Lean.Meta.Grind.Order.NodeId} →
                                                            {cnstrs' :
                                                                Lean.PHashMap Lean.Meta.Sym.ExprPtr
                                                                  (Lean.Meta.Grind.Order.Cnstr
                                                                    Lean.Meta.Grind.Order.NodeId)} →
                                                              {cnstrsOf' :
                                                                  Lean.PHashMap
                                                                    (Lean.Meta.Grind.Order.NodeId ×
                                                                      Lean.Meta.Grind.Order.NodeId)
                                                                    (List
                                                                      (Lean.Meta.Grind.Order.Cnstr
                                                                          Lean.Meta.Grind.Order.NodeId ×
                                                                        Lean.Expr))} →
                                                                {sources' targets' :
                                                                    Lean.PArray
                                                                      (Lean.AssocList Lean.Meta.Grind.Order.NodeId
                                                                        Lean.Meta.Grind.Order.Weight)} →
                                                                  {proofs' :
                                                                      Lean.PArray
                                                                        (Lean.AssocList Lean.Meta.Grind.Order.NodeId
                                                                          Lean.Meta.Grind.Order.ProofInfo)} →
                                                                    {propagate' :
                                                                        List Lean.Meta.Grind.Order.ToPropagate} →
                                                                      { id := id, type := type, u := u,
                                                                            isPreorderInst := isPreorderInst,
                                                                            leInst := leInst, ltInst? := ltInst?,
                                                                            isPartialInst? := isPartialInst?,
                                                                            isLinearPreInst? := isLinearPreInst?,
                                                                            lawfulOrderLTInst? := lawfulOrderLTInst?,
                                                                            ringId? := ringId?,
                                                                            isCommRing := isCommRing,
                                                                            ringInst? := ringInst?,
                                                                            orderedRingInst? := orderedRingInst?,
                                                                            leFn := leFn, ltFn? := ltFn?,
                                                                            nodes := nodes, nodeMap := nodeMap,
                                                                            cnstrs := cnstrs, cnstrsOf := cnstrsOf,
                                                                            sources := sources, targets := targets,
                                                                            proofs := proofs, propagate := propagate } =
                                                                          { id := id', type := type', u := u',
                                                                            isPreorderInst := isPreorderInst',
                                                                            leInst := leInst', ltInst? := ltInst?',
                                                                            isPartialInst? := isPartialInst?',
                                                                            isLinearPreInst? := isLinearPreInst?',
                                                                            lawfulOrderLTInst? := lawfulOrderLTInst?',
                                                                            ringId? := ringId?',
                                                                            isCommRing := isCommRing',
                                                                            ringInst? := ringInst?',
                                                                            orderedRingInst? := orderedRingInst?',
                                                                            leFn := leFn', ltFn? := ltFn?',
                                                                            nodes := nodes', nodeMap := nodeMap',
                                                                            cnstrs := cnstrs', cnstrsOf := cnstrsOf',
                                                                            sources := sources', targets := targets',
                                                                            proofs := proofs',
                                                                            propagate := propagate' } →
                                                                        (id = id' →
                                                                            type = type' →
                                                                              u = u' →
                                                                                isPreorderInst = isPreorderInst' →
                                                                                  leInst = leInst' →
                                                                                    ltInst? = ltInst?' →
                                                                                      isPartialInst? = isPartialInst?' →
                                                                                        isLinearPreInst? =
                                                                                            isLinearPreInst?' →
                                                                                          lawfulOrderLTInst? =
                                                                                              lawfulOrderLTInst?' →
                                                                                            ringId? = ringId?' →
                                                                                              isCommRing = isCommRing' →
                                                                                                ringInst? = ringInst?' →
                                                                                                  orderedRingInst? =
                                                                                                      orderedRingInst?' →
                                                                                                    leFn = leFn' → ⋯) →
                                                                          P