{motive : Mathlib.Explode.Entry → Sort u} →
  (t : Mathlib.Explode.Entry) →
    ((type : Lean.MessageData) →
        (line : Option ℕ) →
          (depth : ℕ) →
            (status : Mathlib.Explode.Status) →
              (thm : Lean.MessageData) →
                (deps : List (Option ℕ)) →
                  (useAsDep : Bool) →
                    motive
                      { type := type, line := line, depth := depth, status := status, thm := thm, deps := deps,
                        useAsDep := useAsDep }) →
      motive t