fixed CHANGELOG: added missing lemma name from agda#2517

jamesmckinna · Dec 30, 2024 · 5180e40 · 5180e40
1 parent c98fdad
commit 5180e40
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -339,8 +339,9 @@ Additions to existing modules
 * In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
   ```agda
   module ⊆-Reasoning
-  concat⁺    : Sublist _⊆_ ass bss → concat ass ⊆ concat bss
-  all⊆concat : (xss : List (List A)) → All (_⊆ concat xss) xss
+  concat⁺               : Sublist _⊆_ ass bss → concat ass ⊆ concat bss
+  xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs ⊆ concat xss
+  all⊆concat            : (xss : List (List A)) → All (_⊆ concat xss) xss
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`: