(motive : Lean.LocalDecl → Sort u_1) →
  (x : Lean.LocalDecl) →
    ((index : ℕ) →
        (fvarId : Lean.FVarId) →
          (n : Lean.Name) →
            (type : Lean.Expr) →
              (bi : Lean.BinderInfo) →
                (kind : Lean.LocalDeclKind) → motive (Lean.LocalDecl.cdecl index fvarId n type bi kind)) →
      ((index : ℕ) →
          (fvarId : Lean.FVarId) →
            (n : Lean.Name) →
              (type value : Lean.Expr) →
                (kind : Lean.LocalDeclKind) → motive (Lean.LocalDecl.ldecl index fvarId n type value true kind)) →
        ((index : ℕ) →
            (fvarId : Lean.FVarId) →
              (n : Lean.Name) →
                (type value : Lean.Expr) →
                  (kind : Lean.LocalDeclKind) → motive (Lean.LocalDecl.ldecl index fvarId n type value false kind)) →
          motive x