CHANGELOG.

CHANGELOG.md

@@ -61,6 +61,11 @@ API-breaking change is listed.
 - Rename instances `option_mbind_proper` → `option_bind_proper` and
   `option_mjoin_proper` → `option_join_proper` to be consistent with similar
   instances for sets and lists.
+- Misc improvements to `head` and `tail` functions for lists:
+  + Define `head l` as notation for `l !! 0` (we had no lemmas about `head`, so
+    now we can use all the `!!` lemmas).
+  + Declare `tail` as `simpl nomatch`.
+  + Add lemmas about `tail`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):