simplify an import

UniMath · Feb 14, 2025 · 1053da1 · 1053da1
1 parent 635e5bd
commit 1053da1
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 6 deletions.
diff --git a/src/literature/100-theorems.lagda.md b/src/literature/100-theorems.lagda.md
@@ -41,9 +41,8 @@ theorem.
 
 ```agda
 open import foundation.cantor-schroder-bernstein-escardo using
-  ( Cantor-Schröder-Bernstein-Escardó)
-open import foundation.cantor-schroder-bernstein-escardo using
-  ( Cantor-Schröder-Bernstein)
+  ( Cantor-Schröder-Bernstein-Escardó ;
+    Cantor-Schröder-Bernstein)
 ```
 
 ### 44. The binomial theorem {#44}

diff --git a/src/literature/1000plus-theorems.lagda.md b/src/literature/1000plus-theorems.lagda.md
@@ -54,9 +54,8 @@ theorem.
 
 ```agda
 open import foundation.cantor-schroder-bernstein-escardo using
-  ( Cantor-Schröder-Bernstein-Escardó)
-open import foundation.cantor-schroder-bernstein-escardo using
-  ( Cantor-Schröder-Bernstein)
+  ( Cantor-Schröder-Bernstein-Escardó ;
+    Cantor-Schröder-Bernstein)
 ```
 
 ### Cantor's theorem {#Q474881}