Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1364:ea44c917ca61

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 20 Jun 2023 15:11:47 +0900
parents abe89e354e4f
children 4e1150abfb86
files src/bijection.agda
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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 ))