(motive : Lean.ConstantKind → Sort u_1) →
  (x : Lean.ConstantKind) →
    (Unit → motive Lean.ConstantKind.defn) →
      (Unit → motive Lean.ConstantKind.thm) →
        (Unit → motive Lean.ConstantKind.axiom) →
          (Unit → motive Lean.ConstantKind.opaque) →
            (Unit → motive Lean.ConstantKind.quot) →
              (Unit → motive Lean.ConstantKind.induct) →
                (Unit → motive Lean.ConstantKind.ctor) → (Unit → motive Lean.ConstantKind.recursor) → motive x