# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687241507 -32400
# Node ID ea44c917ca61faf98f66d04c0c952b5975d5df6e
# Parent  abe89e354e4f2ccecb622c316824a3ca58463fd6
...

diff -r abe89e354e4f -r ea44c917ca61 src/bijection.agda
--- a/src/bijection.agda	Tue Jun 20 12:52:47 2023 +0900
+++ b/src/bijection.agda	Tue Jun 20 15:11:47 2023 +0900
@@ -672,7 +672,7 @@
     ... | case2 lt = there (clist-more {suc i} {n} lt {c} (here px) )
 
     clist-any : (n i : ℕ) → i ≤ n → Any (_≡_ (g (f (fun← an i)))) (clist (c n))
-    clist-any n i i≤n = clist-more ? (lem00 (c i) (c< i))   where
+    clist-any n i i≤n = clist-more (c-mono _ _ i≤n) (lem00 (c i) (c< i))   where
         lem00 : (j : ℕ ) → fun→ cn (g (f (fun← an i))) ≤ j → Any (_≡_ (g (f (fun← an i)))) (clist j)
         lem00 0 f≤j with  ≤-∨ f≤j
         ... | case1 eq = here ( trans (sym (fiso← cn _)) ( cong (fun← cn) eq ))