{motive : Lean.Meta.Grind.Order.State → Sort u} →
  (t : Lean.Meta.Grind.Order.State) →
    ((structs : Array Lean.Meta.Grind.Order.Struct) →
        (typeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)) →
          (exprToStructId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ) →
            (termMap termMapInv : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr)) →
              motive
                { structs := structs, typeIdOf := typeIdOf, exprToStructId := exprToStructId, termMap := termMap,
                  termMapInv := termMapInv }) →
      motive t