{motive : Lean.ConstantKind → Sort u} →
  (t : Lean.ConstantKind) →
    motive Lean.ConstantKind.thm →
      motive Lean.ConstantKind.axiom →
        motive Lean.ConstantKind.ctor →
          motive Lean.ConstantKind.defn → (Nat.hasNotBit 71 t.ctorIdx → motive t) → motive t