diff --git a/CHANGELOG.md b/CHANGELOG.md
index 079989202e4dc4923ceb3c30f3db5012efd0940c..1d11d393074660c6864f4e013ad6b97bb81b1b56 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -46,6 +46,9 @@ With this release, we dropped support for Coq 8.9.
   key, including support for persistent read-only ownership through `dfrac`.
   See `theories/algebra/lib/gmap_view.v` for further information.
   NOTE: The API surface for `gmap_view` is experimental and subject to change.
+* Move the `*_validI` and `*_equivI` lemmas to a new module, `base_logic.algebra`.
+  That module is exported by `base_logic.base_logic` so it should usually be
+  available everywhere without further changes.
 
 **Changes in `proofmode`:**
 
@@ -96,6 +99,10 @@ With this release, we dropped support for Coq 8.9.
   the state interpretation of WP and since `_ctx` is elsewhere used as a suffix
   indicating "this is a persistent assumption that clients should always have in
   their context". Likewise, rename `proph_map_ctx` to `proph_map_interp`.
+* Move `uPred.prod_validI`, `uPred.option_validI`, and
+  `uPred.discrete_fun_validI` to the new `base_logic.algebra` module. That
+  module is exported by `base_logic.base_logic` so these names are now usually
+  available everywhere, and no longer inside the `uPred` module.
 
 **Changes in `program_logic`:**
 
diff --git a/theories/base_logic/algebra.v b/theories/base_logic/algebra.v
index 6c86be60b5ad0b675a813af54849125029248961..d185f4a17e814a11003842cec8fa7569ce1a2510 100644
--- a/theories/base_logic/algebra.v
+++ b/theories/base_logic/algebra.v
@@ -196,7 +196,6 @@ Section auth.
   Implicit Types a b : A.
   Implicit Types x y : auth A.
 
-  (** Internalized properties *)
   Lemma auth_auth_frac_validI q a : ✓ (●{q} a) ⊣⊢@{uPredI M} ✓ q ∧ ✓ a.
   Proof.
     apply view_auth_frac_validI=> n. uPred.unseal; split; [|by intros [??]].