∀ (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_1 : ℕ) (type_1 : Lean.Expr) (u_1 : Lean.Level)
  (isPreorderInst_1 leInst_1 : Lean.Expr)
  (ltInst?_1 isPartialInst?_1 isLinearPreInst?_1 lawfulOrderLTInst?_1 : Option Lean.Expr) (ringId?_1 : Option ℕ)
  (isCommRing_1 : Bool) (ringInst?_1 orderedRingInst?_1 : Option Lean.Expr) (leFn_1 : Lean.Expr)
  (ltFn?_1 : Option Lean.Expr) (nodes_1 : Lean.PArray Lean.Expr)
  (nodeMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Order.NodeId)
  (cnstrs_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Meta.Grind.Order.Cnstr Lean.Meta.Grind.Order.NodeId))
  (cnstrsOf_1 :
    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_1 targets_1 : Lean.PArray (Lean.AssocList Lean.Meta.Grind.Order.NodeId Lean.Meta.Grind.Order.Weight))
  (proofs_1 : Lean.PArray (Lean.AssocList Lean.Meta.Grind.Order.NodeId Lean.Meta.Grind.Order.ProofInfo))
  (propagate_1 : 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_1, type := type_1, u := u_1, isPreorderInst := isPreorderInst_1, leInst := leInst_1,
        ltInst? := ltInst?_1, isPartialInst? := isPartialInst?_1, isLinearPreInst? := isLinearPreInst?_1,
        lawfulOrderLTInst? := lawfulOrderLTInst?_1, ringId? := ringId?_1, isCommRing := isCommRing_1,
        ringInst? := ringInst?_1, orderedRingInst? := orderedRingInst?_1, leFn := leFn_1, ltFn? := ltFn?_1,
        nodes := nodes_1, nodeMap := nodeMap_1, cnstrs := cnstrs_1, cnstrsOf := cnstrsOf_1, sources := sources_1,
        targets := targets_1, proofs := proofs_1, propagate := propagate_1 }) =
    (id = id_1 ∧
      type = type_1 ∧
        u = u_1 ∧
          isPreorderInst = isPreorderInst_1 ∧
            leInst = leInst_1 ∧
              ltInst? = ltInst?_1 ∧
                isPartialInst? = isPartialInst?_1 ∧
                  isLinearPreInst? = isLinearPreInst?_1 ∧
                    lawfulOrderLTInst? = lawfulOrderLTInst?_1 ∧
                      ringId? = ringId?_1 ∧
                        isCommRing = isCommRing_1 ∧
                          ringInst? = ringInst?_1 ∧
                            orderedRingInst? = orderedRingInst?_1 ∧
                              leFn = leFn_1 ∧ ltFn? = ltFn?_1 ∧ nodes = nodes_1 ∧ ⋯)