{motive : Lean.ExternEntry → Sort u} →
  ((backend : Lean.Name) → motive (Lean.ExternEntry.adhoc backend)) →
    ((backend : Lean.Name) → (pattern : String) → motive (Lean.ExternEntry.inline backend pattern)) →
      ((backend : Lean.Name) → (fn : String) → motive (Lean.ExternEntry.standard backend fn)) →
        motive Lean.ExternEntry.opaque → (t : Lean.ExternEntry) → motive t