{motive_1 : Lean.MessageData → Sort u} →
  (t : Lean.MessageData) →
    ((f : Option Lean.PPContext → BaseIO Dynamic) →
        (hasSyntheticSorry : Lean.MetavarContext → Bool) → motive_1 (Lean.MessageData.ofLazy f hasSyntheticSorry)) →
      ((a : Lean.MessageDataContext) → (a_1 : Lean.MessageData) → motive_1 (Lean.MessageData.withContext a a_1)) →
        ((a : Lean.NamingContext) → (a_1 : Lean.MessageData) → motive_1 (Lean.MessageData.withNamingContext a a_1)) →
          ((a : ℕ) → (a_1 : Lean.MessageData) → motive_1 (Lean.MessageData.nest a a_1)) →
            ((a : Lean.MessageData) → motive_1 a.group) →
              ((a a_1 : Lean.MessageData) → motive_1 (a.compose a_1)) →
                ((a : Lean.Name) → (a_1 : Lean.MessageData) → motive_1 (Lean.MessageData.tagged a a_1)) →
                  ((data : Lean.TraceData) →
                      (msg : Lean.MessageData) →
                        (children : Array Lean.MessageData) → motive_1 (Lean.MessageData.trace data msg children)) →
                    (Nat.hasNotBit 2040 t.ctorIdx → motive_1 t) → motive_1 t