naming in changelog

CHANGELOG.md

@@ -60,10 +60,10 @@ lemma.
   To retain backwards compatibility with the interaction laws of fancy updates
   with the plainly modality (`BiFUpdPlainly`), which are incompatible with
   later credits, the logic is parameterized by two typeclasses, `HasLc`
-  and `HasNoLc` that allow opting for either later credits or `BiFUpdPlainly`.
+  and `HasNoLc`, that allow opting for either later credits or `BiFUpdPlainly`.
   The soundness lemmas for the fancy update modality are available in two versions,
   with later credits (suffix `_lc`) and without later credits (suffix `_no_lc`).
-  The lemma `step_fupdN_soundness` is now generic over this choice.
+  The lemma `step_fupdN_soundness_gen` is generic over this choice.
 
 **Changes in `program_logic`:**
 
@@ -78,9 +78,9 @@ lemma.
     and one without support for later credits, providing `HasNoLc` (suffix `_no_lc`).
     Clients of the adequacy proof will need to opt for either of these and introduce
     the additional assumptions.
-  + The parameter for the stuckness bit `s` in `wp_strong_adequacy` has moved up and
-    is now universally quantified in the lemma instead of being existentially quantified
-    at the Iris-level. For clients that already previously quantified over `s`
+  + The parameter for the stuckness bit `s` in `wp_strong_adequacy{_lc, _no_lc}` has
+    moved up and is now universally quantified in the lemma instead of being existentially
+    quantified at the Iris-level. For clients that already previously quantified over `s`
     at the Coq level, the only required change should be to remove the instantiation
     of the existential quantifier.