Add CHANGELOG_NEXT entries

Author: mattpolzin

CHANGELOG_NEXT.md

@@ -39,9 +39,24 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Added append `(++)` for `List` version of `All`.
 
+* Moved helpers and theorems from contrib's `Data.HVect` into base's
+  `Data.Vect.Quantifiers.All` namespace. Some functions were renamed and some
+  already existed. Others had quantity changes -- in short, there were some
+  breaking changes here in addition to removing the respective functions from
+  contrib. If you hit a breaking change, please take a look at
+  https://github.com/idris-lang/Idris2/pull/3191/files and determine if you
+  simply need to update a function name or if your use-case requires additional
+  code changes in the base library. If it's the latter, open a bug ticket or
+  start a discussion on the Idris Discord to determine the best path forward.
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.
 
 * Existing `System.Console.GetOpt` was extended to support errors during options
   parsing in a backward-compatible way.
+
+* Moved helpers from `Data.HVect` to base library's `Data.Vect.Quantifiers.All`
+  and removed `Data.HVect` from contrib. See the additional notes in the
+  CHANGELOG under the `Library changes`/`Base` section above.
+