(motive : Lean.Declaration → Sort u_1) →
  (decl : Lean.Declaration) →
    ((val : Lean.DefinitionVal) → motive (Lean.Declaration.defnDecl val)) →
      ((val : List Lean.DefinitionVal) → motive (Lean.Declaration.mutualDefnDecl val)) →
        ((x : Lean.Declaration) → motive x) → motive decl