{motive : Lean.Meta.Grind.Order.Struct → Sort u} →
  (t : Lean.Meta.Grind.Order.Struct) →
    ((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) →
                                        motive
                                          { 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 }) →
      motive t