{motive : Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind✝ → Sort u} →
  (t : Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind✝¹) →
    motive Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind.div✝ →
      motive Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind.mod✝ →
        motive Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind.sub✝ →
          motive Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind.pow✝ →
            motive Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind.neg✝ →
              motive Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind.natAbs✝ →
                motive Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind.toNat✝ →
                  motive Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind.natCast✝ →
                    motive Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind.toInt✝ →
                      motive Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind.finVal✝ →
                        motive Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind.finMk✝ →
                          (Nat.hasNotBit 16376 (Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind.ctorIdx✝ t) → motive t) →
                            motive t