(motive : Lean.Declaration → Sort u_1) →
  (decl : Lean.Declaration) →
    ((n : Lean.Name) →
        (levelParams : List Lean.Name) →
          (type value : Lean.Expr) →
            (hints : Lean.ReducibilityHints) →
              (safety : Lean.DefinitionSafety) →
                (all : List Lean.Name) →
                  motive
                    (Lean.Declaration.defnDecl
                      { name := n, levelParams := levelParams, type := type, value := value, hints := hints,
                        safety := safety, all := all })) →
      ((n : Lean.Name) →
          (levelParams : List Lean.Name) →
            (type value : Lean.Expr) →
              (all : List Lean.Name) →
                motive
                  (Lean.Declaration.thmDecl
                    { name := n, levelParams := levelParams, type := type, value := value, all := all })) →
        ((x : Lean.Declaration) → motive x) → motive decl