# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687334715 -32400
# Node ID 3bcff593255e4aac1fb28181b97c7e1e77e7b5fa
# Parent  43471e03d6fe325fba5fbc673792e6859c0766d5
...

diff -r 43471e03d6fe -r 3bcff593255e src/bijection.agda
--- a/src/bijection.agda	Wed Jun 21 14:46:51 2023 +0900
+++ b/src/bijection.agda	Wed Jun 21 17:05:15 2023 +0900
@@ -697,14 +697,14 @@
             lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ suc n) → (a : any-cl (suc i) cl) → suc i < ca-list cl
             lem30 0 cl i≤n a = begin
                 2 ≤⟨ s≤s (s≤s z≤n) ⟩ 
-                suc (suc (ca-list (del 1 (del 0 cl a) ?) ))  ≡⟨ ? ⟩ 
-                suc (ca-list (del 1 cl ?) )  ≡⟨ ? ⟩ 
+                suc (suc (ca-list (del 0 (del 1 cl a) (del-any 0 cl a)) ))  ≡⟨ cong suc ( del-ca 0 (del 1 cl a) (del-any 0 cl a) )  ⟩ 
+                suc (ca-list (del 1 cl a) )  ≡⟨ del-ca 1 cl a ⟩ 
                 ca-list cl ∎ where
                    open ≤-Reasoning
-            -- <-transʳ ? (subst (λ k → ca-list (del ? cl ?) < k) (a-list-ca ? ? (a _ ≤-refl))  a<sa )
             lem30 (suc i) cl i≤n a = begin
-               suc (suc (suc i))   ≤⟨ s≤s (lem30 i (del (suc i) cl  a  ) (≤-trans a≤sa i≤n) (del-any (suc i) cl a)) ⟩ 
-               suc (ca-list (del (suc i) cl a))  ≡⟨ del-ca (suc i) cl a ⟩ 
+               suc (suc (suc i))   ≤⟨ s≤s (lem30 i (del (suc i) (del (suc (suc i)) cl a )  
+                    (del-any (suc i) cl a)  ) (≤-trans a≤sa i≤n) (del-any (suc i) cl a)) ⟩ 
+               suc (ca-list (del (suc i) cl (del-any (suc i) cl a)))  ≡⟨ del-ca (suc i) cl (del-any (suc i) cl a) ⟩ 
                ca-list cl ∎ where
                    open ≤-Reasoning
             lem31 : suc n < ca-list (clist (c (suc n)))