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

diff -r e5e592584382 -r 43471e03d6fe src/bijection.agda
--- a/src/bijection.agda	Wed Jun 21 13:24:54 2023 +0900
+++ b/src/bijection.agda	Wed Jun 21 14:46:51 2023 +0900
@@ -685,17 +685,23 @@
          --  induction on n is no good, because (ani (suc n)) may happen in clist (c n)
          --  so we cannot recurse on n<ca-list itself.
          --
-         del : (i : ℕ) → (cl : List C) → any-cl (suc i) cl → List C   -- del 0 contains ani 0
+         del : (i : ℕ) → (cl : List C) → any-cl i cl → List C   -- del 0 contains ani 0
          del = ?
-         del-any : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl)  → any-cl i (del i cl a )
+         del-any : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl)  → any-cl i (del (suc i) cl a )
          del-any = ?
-         del-ca : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl  )
+         del-ca : (i : ℕ) → (cl : List C) → (a : any-cl i cl  )
               → suc (ca-list cl) ≡ ca-list (del i cl a)
          del-ca = ?
          lem06 : suc n < ca-list (clist (c (suc n)))
          lem06 = lem31 where
             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 = ?
+            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 ?) )  ≡⟨ ? ⟩ 
+                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 ⟩