{motive : Lean.ConstantInfo → Sort u} →
  (t : Lean.ConstantInfo) →
    ((val : Lean.DefinitionVal) → motive (Lean.ConstantInfo.defnInfo val)) →
      ((val : Lean.TheoremVal) → motive (Lean.ConstantInfo.thmInfo val)) →
        ((val : Lean.OpaqueVal) → motive (Lean.ConstantInfo.opaqueInfo val)) →
          (Nat.hasNotBit 14 t.ctorIdx → motive t) → motive t