# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687158105 -32400
# Node ID e3d3749e80bd3955e3be638546dfca5ea53837e2
# Parent  88356bb882d48c92c39c0b9ac2bf9eb58b3864f5
...

diff -r 88356bb882d4 -r e3d3749e80bd src/bijection.agda
--- a/src/bijection.agda	Mon Jun 19 12:40:47 2023 +0900
+++ b/src/bijection.agda	Mon Jun 19 16:01:45 2023 +0900
@@ -484,13 +484,8 @@
 -- Bernstein is non constructive, so we cannot use this without some assumption
 --   but in case of ℕ, we can construct it directly.
 
-open import Data.Product
-open import Relation.Nary using (⌊_⌋)
-open import Relation.Nullary.Decidable hiding (⌊_⌋)
-open import Data.Unit.Base using (⊤ ; tt)
-open import Data.List.Fresh hiding ([_])
-open import Data.List.Fresh.Relation.Unary.Any
-open import Data.List.Fresh.Relation.Unary.All
+open import Data.List hiding ([_])
+open import Data.List.Relation.Unary.Any
 
 record InjectiveF (A B : Set) : Set where
    field
@@ -545,40 +540,6 @@
     ... | yes isb = suc (count-A n)
     ... | no nisb = count-A n
 
-    count-A-mono : {i j : ℕ} → i ≤ j → count-A i ≤ count-A j
-    count-A-mono {i} {j} i≤j with ≤-∨ i≤j
-    ... | case1 refl = ≤-refl
-    ... | case2 i<j = lem00 _ _ i<j where
-         lem00 : (i j : ℕ) → i < j → count-A i ≤ count-A j
-         lem00 i (suc j) (s≤s i<j) = ≤-trans (count-A-mono i<j) (lem01 j) where
-             lem01 : (j : ℕ) → count-A j ≤ count-A (suc j)
-             lem01 zero with is-A (fun← cn (suc zero))
-             ... | yes isb = refl-≤s
-             ... | no nisb = ≤-refl
-             lem01 (suc n) with is-A (fun← cn (suc (suc n)))
-             ... | yes isb = refl-≤s
-             ... | no nisb = ≤-refl
-
-    count-A<i : (i : ℕ) → count-A i ≤ suc i
-    count-A<i zero with is-A (fun← cn  zero) | inspect ( count-A ) zero
-    ... | yes isa | record { eq = eq1 } = ≤-refl
-    ... | no nisa | record { eq = eq1 } = refl-≤s
-    count-A<i (suc i) with is-A (fun← cn  (suc i)) | inspect ( count-A ) (suc i)
-    ... | yes isa | record { eq = eq1 } = s≤s ( count-A<i i )
-    ... | no nisa | record { eq = eq1 } = ≤-trans (count-A<i i ) refl-≤s
-
-    full-a : (i : ℕ) → i < count-A i → Is A C (λ x → g (f x)) (fun← cn i)
-    full-a zero i<ci with is-A (fun← cn  zero) | inspect ( count-A ) zero
-    ... | yes isa | record { eq = eq1 } = isa
-    ... | no nisa | record { eq = eq1 } = ⊥-elim ( nat-≡< refl i<ci )
-    full-a (suc i) i<ci with is-A (fun← cn  (suc i)) | inspect ( count-A ) (suc i)
-    ... | yes isa | record { eq = eq1 } = isa
-    ... | no nisa | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans lem36 lem39) a<sa ) where
-          lem36 : suc (suc i) ≤ count-A i
-          lem36 = i<ci
-          lem39 : count-A i ≤ suc i
-          lem39 = count-A<i i
-
     ¬isA∧isB : (y : C ) →  Is A C (λ x → g ( f x)) y → ¬ Is B C g y → ⊥
     ¬isA∧isB y isa nisb = ⊥-elim ( nisb record { a = f (Is.a isa) ; fa=c = lem } ) where
          lem : g (f (Is.a isa)) ≡ y
@@ -606,98 +567,14 @@
     c zero = fun→ cn (g (f (fun← an zero)))
     c (suc n) = max (fun→ cn (g (f (fun← an (suc n))))) (c n)
 
-
     c< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (c n)
     c< zero zero (s≤s z≤n) = a<sa
     c< (suc i) zero  (s≤s ())
     c< zero (suc n) (s≤s z≤n) = ≤-trans (c< zero n (<-transʳ  z≤n a<sa) ) (s≤s (y≤max (fun→ cn (g (f (fun← an (suc n))))) (c n)))
     c< (i @ (suc _)) (suc n) i≤n with ≤-∨ i≤n
     ... | case1 refl = s≤s (x≤max  (fun→ cn (g (f (fun← an (suc n))))) (c n))
-    ... | case2 (s≤s (s≤s i<n)) = ≤-trans (c< i n (<-transʳ i<n a<sa)) (s≤s (y≤max (fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n))))) (c n)))
-
-    --  (c1 n i) is number of a which fun← an a ≤ n ∧ fun→ cn (g (f a)) < i ∧ g (f a) is A
-
-    c1 : (n i : ℕ) → ℕ
-    c1 zero i with <-cmp (fun→ cn (g (f (fun← an zero)))) i
-    ... | tri< a ¬b ¬c = 1
-    ... | tri≈ ¬a b ¬c = 1
-    ... | tri> ¬a ¬b c₁ = 0
-    c1 (suc n) i with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i
-    ... | tri< a ¬b ¬c = suc (c1 n i)
-    ... | tri≈ ¬a b ¬c = suc (c1 n i)
-    ... | tri> ¬a ¬b c₁ = c1 n i
-
-    c1-mono : {n i j : ℕ} → i ≤ j  → (c1 n i ≡ c1 n j) ∨ (c1 n i < c1 n j)
-    c1-mono {zero} {i} {j} le with <-cmp (fun→ cn (g (f (fun← an zero)))) i  | <-cmp (fun→ cn (g (f (fun← an zero)))) j
-    ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = case1 refl
-    ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = case1 refl
-    ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> le (<-trans c₁ a) )
-    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = case1 refl
-    ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = case1 refl
-    ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) le) c₁  )
-    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = case2 ≤-refl
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = case2 ≤-refl
-    ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = case1 refl
-    c1-mono {suc n} {zero} {zero} z≤n = case1 refl
-    c1-mono {suc n} {zero} {suc j} z≤n with <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero  | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc j)
-        | c1-mono {n} {zero} {suc j} z≤n
-    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case1 eq = case1 (cong suc eq)
-    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case2 le = case2 ( s≤s le )
-    ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case1 eq = case1 (cong suc eq)
-    ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case2 le = case2 ( s≤s le )
-    ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | _ = ⊥-elim ( nat-≡< (sym b) (≤-trans (s≤s z≤n) c₁)  )
-    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n zero) ≤ k ) (cong suc eq) ≤-refl )
-    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case2 le = case2 (≤-trans le refl-≤s )
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n zero) ≤ k ) (cong suc eq) ≤-refl )
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case2 le = case2 (≤-trans le refl-≤s )
-    ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | case1 eq = case1 eq
-    ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | case2 le = case2 le
-    c1-mono {suc n} {suc i} {suc j} (s≤s le) with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc j)
-         | c1-mono {n} {suc i} {suc j} (s≤s le)
-    ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | case1 eq = case1 (cong suc eq)
-    ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | case2 le = case2 (s≤s le)
-    ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | case1 eq = case1 (cong suc eq)
-    ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | case2 le = case2 (s≤s le)
-    ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ | u = ⊥-elim ( nat-≤> (s≤s le) (<-transˡ c₁ (≤-trans refl-≤s a ) ))
-    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case1 eq = case1 (cong suc eq)
-    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | case2 le = case2 (s≤s le)
-    ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case1 eq = case1 (cong suc eq)
-    ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | case2 le = case2 (s≤s le)
-    ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | u = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) (s≤s le)) c₁  )
-    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n (suc i)) ≤ k ) (cong suc eq) ≤-refl )
-    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | case2 le = case2 (≤-trans le refl-≤s )
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case1 eq = case2 ( subst (λ k → suc (c1 n (suc i)) ≤ k ) (cong suc eq) ≤-refl )
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | case2 le = case2 (≤-trans le refl-≤s )
-    ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | u = u
-
-    c1-max : (n i : ℕ) → c n < i → c1 n i ≡ suc n
-    c1-max zero i cn<i with <-cmp (fun→ cn (g (f (fun← an zero)))) i
-    ... | tri< a ¬b ¬c = refl
-    ... | tri≈ ¬a b ¬c = refl
-    ... | tri> ¬a ¬b c₁ = ⊥-elim (c100 cn<i)  where
-       c100 : ¬ ( suc (fun→ cn (g ( f ( fun← an 0)))) ≤ i )
-       c100 f<i = nat-≤> (s≤s c₁) (<-transʳ f<i (<-trans a<sa a<sa))
-    c1-max (suc n) i cn<i = c101 where
-        m<i : fun→ cn (g (f (fun← an (suc n))))  < i
-        m<i = begin
-           suc (fun→ cn (g (f (fun← an (suc n)))))  ≤⟨ s≤s (x≤max _ _) ⟩
-           suc (max (fun→ cn (g (f (fun← an (suc n))))) (c n))  ≤⟨ cn<i ⟩
-           i ∎ where
-             open ≤-Reasoning
-        c102 : c n < i
-        c102 = begin
-           suc (c n)  ≤⟨ s≤s (y≤max _ _) ⟩
-           suc (max (fun→ cn (g (f (fun← an (suc n))))) (c n))  ≤⟨ cn<i ⟩
-           i ∎ where
-             open ≤-Reasoning
-        c101 : c1 (suc n) i ≡ suc (suc n)
-        c101 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) i
-        ... | tri< a ¬b ¬c = cong suc (c1-max n i c102 )
-        ... | tri≈ ¬a b ¬c = cong suc (c1-max n i c102 )
-        ... | tri> ¬a ¬b c₁ = ⊥-elim ( nat-<> c₁ m<i )
-
-    gf-is-a :  (i : ℕ) → Is A C (λ i → g (f i)) (g (f (fun← an i)))
-    gf-is-a i = record { a = fun← an i ; fa=c = refl }
+    ... | case2 (s≤s (s≤s i<n)) = ≤-trans (c< i n (<-transʳ i<n a<sa)) 
+        (s≤s (y≤max (fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n))))) (c n)))
 
     inject-cgf : {i j : ℕ} → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j))) → i ≡ j
     inject-cgf {i} {j} eq = bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi ( bi-inject→ cn eq )))
@@ -705,387 +582,60 @@
     ani : (i : ℕ) → ℕ
     ani i = fun→ cn (g (f (fun← an i)))
 
-    i-in-n : (i n : ℕ) → i ≤ n → Set
-    i-in-n i n i≤n = c1 n (suc (c n)) ≤ i
+    -- if a list contains n different A, length of list is greater than n
 
-    --- c1 n i
-    c1+1P : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn (suc i))) →  Set
-    c1+1P n i isa with <-cmp n (fun→  an (Is.a isa))
-    ... | tri< n<an ¬b ¬c = c1 n i ≡ c1 n (suc i)
-    ... | tri≈ ¬a n=an ¬c = suc (c1 n i) ≡ c1 n (suc i)
-    ... | tri> ¬a ¬b an<n = suc (c1 n i) ≡ c1 n (suc i)
+    record NL (n : ℕ) : Set where
+       field 
+          nlist : List A
+          anyn : (i : ℕ) → i ≤ n →  Any (λ y → fun← an i ≡ y) nlist
 
-    c1+1 : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn (suc i)))
-        →  c1+1P n i isa
-    c1+1 0 i isa with <-cmp 0 (fun→  an (Is.a isa))
-    ... | tri< n<an ¬b ¬c = c123 where
-         c123 : c1 zero i ≡ c1 zero (suc i)
-         c123 with <-cmp (ani 0) i | <-cmp (ani 0) (suc i)
-         ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = refl
-         ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = refl
-         ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> refl-≤s (<-trans c₁ a) )
-         ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = refl
-         ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl
-         ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa ) c₁  )
-         ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = ⊥-elim ( nat-≤> a (s≤s c₁))
-         ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = refl
-         ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nat-≡< c126 n<an ) where
-               open ≡-Reasoning
-               c127 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡ fun→ cn (g (f (fun← an 0)))
-               c127 = begin
-                  fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
-                  fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
-                  fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
-                  suc i ≡⟨ sym b ⟩
-                  fun→ cn (g (f (fun← an 0))) ∎
-               c126 : 0 ≡ fun→ an (Is.a isa)
-               c126 = begin
-                  0 ≡⟨ sym ( inject-cgf c127) ⟩
-                  fun→ an (Is.a isa) ∎
-    ... | tri≈ ¬a n=an ¬c = c124 where
-         open ≡-Reasoning
-         c125 : fun→ cn (g (f (fun← an 0))) ≡ suc i
-         c125 = begin
-            fun→ cn (g (f (fun← an 0))) ≡⟨ cong (λ k → fun→ cn (g (f (fun← an k)))) n=an ⟩
-            fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ≡⟨  cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
-            fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
-            fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
-            suc i ∎
-         c124 : suc (c1 zero i) ≡ c1 zero (suc i)
-         c124 with <-cmp (ani 0) i | <-cmp (ani 0) (suc i)
-         ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≤> a (<-trans a<sa (subst (λ k → suc i < suc k ) (sym c125) (s≤s a<sa) )))
-         ... | tri≈ ¬a b ¬c | _ = ⊥-elim ( nat-≡< (sym b) (subst (λ k → i < k) (sym c125) a<sa ))
-         ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = refl
-         ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = refl
-         ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ⊥-elim ( ¬b₁ c125 )
-    c1+1 (suc n) i isa with <-cmp (suc n) (fun→  an (Is.a isa))
-    ... | tri< n<an ¬b ¬c = c115 where
-         open ≡-Reasoning
-         c110 : c1 n i ≡ c1 n (suc i)
-         c110 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
-         ... | tri< a ¬b ¬c | s = s
-         ... | tri≈ ¬a b ¬c | s = ⊥-elim ( nat-≡< b (<-trans a<sa n<an ))
-         ... | tri> ¬a ¬b c₁ | s = ⊥-elim ( nat-≤> c₁ (<-trans (<-trans a<sa a<sa) (<-transʳ n<an a<sa ) ))
-         c115 : c1 (suc n) i ≡ c1 (suc n) (suc i)
-         c115 with <-cmp (ani (suc n)) i | <-cmp (ani (suc n)) (suc i)
-         ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = cong suc c110
-         ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = cong suc c110
-         ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> a≤sa (<-transˡ c₁ (≤-trans refl-≤s a ) ))
-         ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = cong suc c110
-         ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = cong suc c110
-         ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa ) c₁  )
-         ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a))
-         ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< c130 n<an) where
-              c118 : fun→ cn (g (f (fun← an (suc n)))) ≡ suc i
-              c118 = b
-              c128 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡ suc i
-              c128 = begin
-                  fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
-                  fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
-                  fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
-                  suc i ∎
-              c130 : suc n ≡ fun→ an (Is.a isa)
-              c130 = inject-cgf (trans c118 (sym c128 ))
-         ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = c110
-    ... | tri≈ ¬a n=an ¬c = c115 where
-         c111 : c1 n i ≡ c1 n (suc i)
-         c111 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
-         ... | tri< a ¬b ¬c | s = s
-         ... | tri≈ ¬a b ¬c | s = ⊥-elim ( nat-≡< b (subst (λ k → n < k ) n=an a<sa ))
-         ... | tri> ¬a ¬b c₁ | s = ⊥-elim ( nat-≡< (sym n=an) (<-trans c₁ a<sa ))
-         open ≡-Reasoning
-         c128 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡ suc i
-         c128 = begin
-              fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
-              fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
-              fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
-              suc i ∎
-         c129 : fun→ cn (g (f (fun← an (suc n))))  ≡ suc i
-         c129 = begin
-              fun→ cn (g (f (fun← an (suc n))))  ≡⟨ cong (λ k → fun→ cn (g (f (fun← an k)))) n=an ⟩
-              fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
-              fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
-              fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
-              suc i ∎
-         c115 : suc (c1 (suc n) i) ≡ c1 (suc n) (suc i)
-         c115 with <-cmp (ani (suc n)) i | <-cmp (ani (suc n)) (suc i)
-         ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≡< c129 (<-trans a a<sa ))
-         ... | tri≈ ¬a b ¬c | _ = ⊥-elim ( nat-≡< (trans (sym b) c129) a<sa )
-         ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a))
-         ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = cong suc c111
-         ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ⊥-elim ( nat-≡< (sym c129) c₂ )
-    ... | tri> ¬a ¬b an<n = c115 where
-         c112 : suc (c1 n i) ≡ c1 n (suc i)
-         c112 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
-         ... | tri< a ¬b ¬c | s = ⊥-elim (nat-≤> an<n (<-transʳ a a<sa) )
-         ... | tri≈ ¬a b ¬c | s = s
-         ... | tri> ¬a ¬b c₁ | s = s
-         open ≡-Reasoning
-         c115 : suc (c1 (suc n) i) ≡ c1 (suc n) (suc i)
-         c115 with <-cmp (ani (suc n)) i | <-cmp (ani (suc n)) (suc i)
-         ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = cong suc c112
-         ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = cong suc c112
-         ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> a≤sa (<-transˡ c₁ (≤-trans refl-≤s a ) ))
-         ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = cong suc c112
-         ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = cong suc c112
-         ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa ) c₁  )
-         ... | tri> ¬a ¬b c₁ | tri< (s≤s a) ¬b₁ ¬c = ⊥-elim (nat-≡< refl (<-transˡ c₁ a))
-         ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nat-≡< (sym c130) an<n )  where
-              c118 : fun→ cn (g (f (fun← an (suc n)))) ≡ suc i
-              c118 = b
-              c128 : fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡ suc i
-              c128 = begin
-                  fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡⟨ cong (λ k → fun→ cn (g (f k))) (fiso← an _) ⟩
-                  fun→ cn (g (f (Is.a isa))) ≡⟨ cong (fun→ cn) (Is.fa=c isa) ⟩
-                  fun→ cn (fun← cn (suc i)) ≡⟨ fiso→ cn _ ⟩
-                  suc i ∎
-              c130 : suc n ≡ fun→ an (Is.a isa)
-              c130 = inject-cgf (trans c118 (sym c128 ))
-         ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = c112
+    remove-n : (n : ℕ) → List A → List A
+    remove-n n [] = []
+    remove-n n (h ∷ t ) with <-cmp n (fun→ an h)
+    ... | tri< a ¬b ¬c = t
+    ... | tri≈ ¬a b ¬c = h ∷ remove-n n t
+    ... | tri> ¬a ¬b c₁ = h ∷ remove-n n t
 
-    c1+0 : {n i : ℕ} → ¬ Is A C (λ x → g (f x)) (fun← cn (suc i)) →  c1 n i ≡ c1 n (suc i)
-    c1+0 {zero} {i} nisa with <-cmp (fun→ cn (g (f (fun← an zero)))) i  | <-cmp (fun→ cn (g (f (fun← an zero)))) (suc i)
-    ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ =  refl
-    ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ =  refl
-    ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> a≤sa (<-trans c₁ a) )
-    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ =  refl
-    ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ =  refl
-    ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa) c₁  )
-    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = ⊥-elim ( nat-≤> a (s≤s c₁))
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = c00 } ) where
-           open ≡-Reasoning
-           c00 : g (f (fun← an 0)) ≡ fun← cn (suc i)
-           c00 = begin
-              g (f (fun← an 0)) ≡⟨ sym (fiso← cn _) ⟩
-              fun← cn (fun→ cn (g (f (fun← an 0))))  ≡⟨ cong (fun← cn) b ⟩
-              fun← cn (suc i) ∎
-    ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ =  refl
-    c1+0 {suc n} {zero}  nisa with <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero  | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc zero)
-        | c1+0 {n} {zero} nisa
-    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | eq =  (cong suc eq)
-    ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | eq =  (cong suc eq)
-    ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | _ = ⊥-elim ( nat-≡< (sym b) (≤-trans (s≤s z≤n) c₁)  )
-    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | eq = ⊥-elim ( nat-≤> a (s≤s c₁))
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | eq = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = c00 } ) where
-           open ≡-Reasoning
-           c00 : g (f (fun← an (suc n))) ≡ fun← cn 1
-           c00 = begin
-              g (f (fun← an (suc n))) ≡⟨ sym (fiso← cn _) ⟩
-              fun← cn (fun→ cn (g (f (fun← an (suc n)))))  ≡⟨ cong (fun← cn) b ⟩
-              fun← cn 1 ∎
-    ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | eq =  eq
-    c1+0 {suc n} {suc i}  nisa with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i) | <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc (suc i))
-         | c1+0 {n} {suc i}  nisa
-    ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | eq =  cong suc eq
-    ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | eq = cong suc eq
-    ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ | u = ⊥-elim ( nat-≤> a≤sa (<-transˡ c₁ (≤-trans refl-≤s a ) ))
-    ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | eq = cong suc eq
-    ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | eq =  cong suc eq
-    ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ | u = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa) c₁  )
-    ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c | eq = ⊥-elim ( nat-≤> a (s≤s c₁))
-    ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c | eq = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = c00 } ) where 
-           open ≡-Reasoning
-           c00 : g (f (fun← an (suc n))) ≡ fun← cn (suc (suc i))
-           c00 = begin
-              g (f (fun← an (suc n))) ≡⟨ sym (fiso← cn _) ⟩
-              fun← cn (fun→ cn (g (f (fun← an (suc n)))))  ≡⟨ cong (fun← cn) b ⟩
-              fun← cn (suc (suc i)) ∎
-    ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ | u = u
+    NL-1 : (n : ℕ) → NL (suc n) → NL n
+    NL-1 n nl = record { nlist = remove-n n (NL.nlist nl) ; anyn = ? } where
+        nl03 : (i : ℕ) → i ≤ n → Any (_≡_ (fun← an i)) (remove-n n (NL.nlist nl))
+        nl03 i i≤n = nl04 _ (NL.anyn nl i ? )  where
+           nl04 : (x : List A) → Any (_≡_ (fun← an i)) x → Any (_≡_ (fun← an i)) (remove-n n x)
+           nl04 (h ∷ t) (here px) with <-cmp n (fun→ an h)
+           ... | tri< a ¬b ¬c = ?
+           ... | tri≈ ¬a b ¬c = here px
+           ... | tri> ¬a ¬b c₁ = here px
+           nl04 (h ∷ t) (there a) with <-cmp n (fun→ an h)
+           ... | tri< a ¬b ¬c = ?
+           ... | tri≈ ¬a b ¬c = there (nl04 t a)
+           ... | tri> ¬a ¬b c₁ = there (nl04 t a)
 
-    c1<ca : (n i : ℕ) → c1 n i ≤ count-A i
-    c1<ca zero zero with is-A (fun← cn zero) |  <-cmp (fun→ cn (g (f (fun← an zero)))) zero
-    ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) b) })
-    ... | no nisa | tri> ¬a ¬b c₁ = ≤-refl
-    ... | yes isa | tri≈ ¬a b ¬c = ≤-refl
-    ... | yes isa | tri> ¬a ¬b c₁ = a≤sa
-    c1<ca (suc n) zero with is-A (fun← cn zero) |  <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero
-    ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) b ) } )
-    ... | no nisa | tri> ¬a ¬b c₁ = lem01 n ≤-refl where
-         lem01 : (i : ℕ) → i ≤ n → c1 i 0 ≤ 0
-         lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
-         ... | tri> ¬a ¬b c₁ = ≤-refl
-         ... | tri≈ ¬a bi ¬c = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) bi) } )
-         lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero
-         ... | tri≈ ¬a bi ¬c = ⊥-elim ( nisa record { a = fun← an (suc i) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) bi) } )
-         lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa)
-    ... | yes isa | tri≈ ¬a b ¬c = lem01 n ≤-refl where
-         lem01 : (i : ℕ) → i ≤ n → suc (c1 i 0) ≤ 1 
-         lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
-         ... | tri> ¬a ¬b c₁ = ≤-refl 
-         ... | tri≈ ¬a bi ¬c = ⊥-elim (nat-≡< (inject-cgf (trans bi (sym b)) ) (<-transʳ i≤n a<sa  ))
-         lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero
-         ... | tri≈ ¬a bi ¬c = ⊥-elim (nat-≡< (inject-cgf (trans bi (sym b)) ) (<-transʳ i≤n a<sa  ))
-         lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa)
-    ... | yes isa | tri> ¬a ¬b c₁ = lem01 n ≤-refl where
-         lem01 : (i : ℕ) → i ≤ n → c1 i 0 ≤ 1 
-         lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
-         ... | tri> ¬a ¬b c₁ = a≤sa
-         ... | tri≈ ¬a bi ¬c = ≤-refl
-         lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero
-         ... | tri≈ ¬a bi ¬c = lem02 i ≤-refl where
-             lem02 : (j : ℕ) → j ≤ i → suc (c1 j 0) ≤ 1
-             lem02 zero j≤i with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
-             ... | tri≈ ¬a bi2 ¬c = ⊥-elim (nat-≡< (sym (inject-cgf (trans bi (sym bi2)) )) (<-transʳ z≤n a<sa  ))
-             ... | tri> ¬a ¬b c₁ = ≤-refl
-             lem02 (suc j) j≤i with <-cmp (fun→ cn (g (f (fun← an (suc j))))) zero
-             ... | tri≈ ¬a bi2 ¬c = ⊥-elim (nat-≡< (sym (inject-cgf (trans bi (sym bi2)) )) (<-transʳ j≤i a<sa  ))
-             lem02 (suc j) (s≤s j≤i) | tri> ¬a ¬b c₁ = lem02 j (≤-trans j≤i a≤sa)
-         lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa)
-    c1<ca zero (suc i) with is-A (fun← cn (suc i)) |  <-cmp (fun→ cn (g (f (fun← an zero)))) (suc i)
-    ... | no nisa | tri< a ¬b ¬c = lem12 where
-         lem12 : 1 ≤ count-A i  -- ca contains ani 0
-         lem12 = ?
-    ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim ( nisa ? )
-    ... | no nisa | tri> ¬a ¬b c₁ = z≤n 
-    ... | yes isa | tri< a ¬b ¬c = s≤s z≤n
-    ... | yes isa | tri≈ ¬a b ¬c = s≤s z≤n
-    ... | yes isa | tri> ¬a ¬b c₁ = z≤n
-    c1<ca (suc n) (suc i) with is-A (fun← cn (suc i)) 
-    ... | no nisa = ca00 where
-       ca00 : c1 (suc n) (suc i) ≤ count-A i
-       ca00 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
-       ... |  tri< a ¬b ¬c = lem12 where -- subst (λ k → k ≤ count-A i) (sym (lem11 n ≤-refl)) lem10 where
-             lem13 : c1 n i ≡ c1 n (suc i) 
-             lem13 = c1+0 {n} {i} nisa
-             lem10 : c1 n i ≤ count-A i
-             lem10 = c1<ca n i
-             lem12 : suc (c1 n (suc i)) ≤ count-A i  -- becase count-A i contains (ani (suc n))
-             lem12 = ?
-       ... |  tri≈ ¬a b ¬c = ⊥-elim (nisa ? )
-       ... |  tri> ¬a ¬b c₁ = subst ( λ k → k ≤ count-A i) (c1+0 {n} {i} nisa) (c1<ca n i)
-    ... | yes isa = ca01 where
-       lem10 : c1 n i ≤ count-A i
-       lem10 = c1<ca n i
-       lem12 : c1 n (suc i) ≤ suc (count-A i) 
-       lem12 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
-       ... | tri< a ¬b ¬c | eq = ≤-trans (subst (λ k → k ≤ count-A i) eq (c1<ca n i)) a≤sa
-       ... | tri≈ ¬a b ¬c | eq = begin
-             c1 n (suc i) ≡⟨ sym eq ⟩
-             suc ( c1 n i) ≤⟨ s≤s (c1<ca n i) ⟩
-             suc (count-A i) ∎ where open ≤-Reasoning
-       ... | tri> ¬a ¬b c₁ | eq = begin
-             c1 n (suc i) ≡⟨ sym eq ⟩
-             suc ( c1 n i) ≤⟨ s≤s (c1<ca n i) ⟩
-             suc (count-A i) ∎ where open ≤-Reasoning
-       ca01 : c1 (suc n) (suc i) ≤ suc (count-A i)
-       ca01 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
-       ... | tri< a ¬b ¬c = lem13 n ≤-refl where  -- count-A contains (suc i), so keep ≤-relation
-             lem13 : (j : ℕ) → j ≤ n → suc (c1 j (suc i)) ≤ suc (count-A i)
-             lem13 0 j≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) (suc i)
-             ... | tri< a ¬b ¬c = ?
-             ... | tri≈ ¬a b ¬c = ?
-             ... | tri> ¬a ¬b c₁ = ?
-             lem13 (suc j) j≤n with <-cmp (fun→ cn (g (f (fun← an (suc j))))) (suc i)
-             ... | tri< a ¬b ¬c = lem16 where
-                  lem16 : suc (suc (c1 j (suc i))) ≤ suc (count-A i)
-                  lem16 = ?
-                  lme14 : suc (c1 j (suc i)) ≤ suc (count-A i)
-                  lme14 = lem13 j ?
-             ... | tri≈ ¬a b ¬c = ? -- cong suc (lem13 j ?)
-             ... | tri> ¬a ¬b c₁ = ?
-       ... | tri≈ ¬a b ¬c = lem13 where  -- count-A contains (suc i) here
-             lem15 : c1 n i ≡ c1 n (suc i) 
-             lem15 with <-cmp n (fun→ an (Is.a isa)) | c1+1 n i isa 
-             ... | tri< a ¬b ¬c | eq = eq
-             ... | tri≈ ¬a bi ¬c | eq = ⊥-elim ( nat-≡< (sym ( inject-cgf ( trans b lem16 ))) a<sa ) where
-                  lem16 : suc i ≡  fun→ cn (g (f (fun← an n )))
-                  lem16 = begin 
-                       suc i ≡⟨ sym ( fiso→ cn _) ⟩
-                       fun→ cn (fun← cn (suc i))  ≡⟨ cong (fun→ cn) (sym (Is.fa=c isa)) ⟩
-                       fun→ cn (g (f (Is.a isa)))  ≡⟨ cong (λ k → fun→ cn (g (f k)) ) (sym (fiso← an _)) ⟩
-                       fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡⟨  cong (λ k → fun→ cn (g (f (fun← an k))))  (sym bi) ⟩
-                       fun→ cn (g (f (fun← an n ))) ∎ where open ≡-Reasoning
-             ... | tri> ¬a ¬b c₁ | eq = ⊥-elim ( nat-≡< refl lem17 ) where
-                  lem18 : fun→ cn (g (f (fun← an (suc n)))) ≡ fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))
-                  lem18 = begin
-                       fun→ cn (g (f (fun← an (suc n)))) ≡⟨ b ⟩
-                       suc i ≡⟨ sym ( fiso→ cn _) ⟩
-                       fun→ cn (fun← cn (suc i)) ≡⟨ sym (cong (fun→ cn) (Is.fa=c isa)) ⟩
-                       fun→ cn (g (f (Is.a isa))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (sym (fiso← an _)) ⟩
-                       fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ∎ where open ≡-Reasoning
-                  lem17 : suc n ≤ n
-                  lem17 = begin
-                       suc n <⟨ s≤s a<sa ⟩
-                       suc (suc n) ≡⟨ cong (λ k → suc k) (inject-cgf lem18 ) ⟩
-                       suc (fun→ an (Is.a isa)) ≤⟨ c₁ ⟩
-                       n ∎ where open ≤-Reasoning
-             lem13 : suc (c1 n (suc i)) ≤ suc (count-A i) 
-             lem13 = s≤s ( subst (λ k → k ≤ count-A i) lem15 ( c1<ca n i) )
-       ... | tri> ¬a ¬b c₁ = lem12 -- count-A is one degree larger now
+    n<list : (n : ℕ) → (nl : NL n) → n ≤ length (NL.nlist nl)
+    n<list 0 nl = z≤n
+    n<list (suc zero) nl = ?
+    n<list (suc (suc n)) nl = ? where
+        nl01 : suc n ≤ length (NL.nlist (NL-1 (suc n) nl))
+        nl01  = n<list (suc n) (NL-1 (suc n) nl)
+        nl00 : length (NL.nlist (NL-1 (suc n) nl)) < length (NL.nlist nl)
+        nl00 = nl02 (suc n) (NL.nlist nl) (NL.anyn nl (suc n) ? )  where
+           nl02 : (n : ℕ) (x : List A) → Any (λ y → fun← an n ≡ y) x → length (remove-n n x) < length x
+           nl02 n (h ∷ ta) (here px) with <-cmp n (fun→ an h)
+           ... | tri< a ¬b ¬c = ≤-refl
+           ... | tri≈ ¬a b ¬c = ?
+           ... | tri> ¬a ¬b c₁ = ?
+           nl02 n (h ∷ ta) (there a) with <-cmp n (fun→ an h)
+           ... | tri< a ¬b ¬c = ≤-refl
+           ... | tri≈ ¬a b ¬c = s≤s (nl02 n ta a)
+           ... | tri> ¬a ¬b c₁ = s≤s (nl02 n ta a)
+     
 
     record maxAC (n : ℕ) : Set where
        field
            ac : ℕ
            n<ca : n < count-A ac
 
-    lem03 : (n : ℕ) → maxAC n
-    lem03 n = record { ac = c1 n (suc (c n)) ; n<ca = ? }
-
-    --
-    -- we have n C sequcence having n A which is less than c n as FList (c n) , so we have n
-    --    c i =  i th FL (c n) where
-    --         ∃ j → i ≡ fun→ cn (g (f (fun← an j)))   by FList n
-    --    cm =     count-A (c n)
-    --    0 < suc (count-A (c 0)) ≡  count-A (suc (c 0)) ≤ count-A (c 1) < ... < suc (count-A (c n)) ≤ count-A (c n)
-    --    0 < cm  →          1 < cm                                                → n < cm
-    -- it means
-    --    n < count-A (c n)
-    --
-
-    cl07 : { i j : ℕ } → suc i < suc j → i < j
-    cl07 {i} {j} (s≤s lt) = lt
-
     lem02 : (n : ℕ) → maxAC n
-    lem02 n = record { ac = c n ; n<ca = n<ca n } where
-         ca+1 : (i : ℕ) → i < fun→ cn (g (f (fun← an i))) → count-A i < count-A (fun→ cn (g (f (fun← an i))))
-         ca+1 i i<ca with fun→ cn (g (f (fun← an i))) | inspect (fun→ cn) (g (f (fun← an i)))
-         ... | suc ca | record { eq = eq1 } with is-A (fun← cn (suc ca))
-         ... | yes isa = <-transʳ ( count-A-mono (px≤py i<ca)) cl22 where
-             cl22 :  count-A (pred (suc ca)) < suc (count-A ca)
-             cl22 = ≤-refl
-         ... | no nisa = ⊥-elim ( nisa record { a = fun← an i ; fa=c = cl21 } ) where
-             cl21 : g (f ( fun← an i)) ≡ fun← cn (suc ca)
-             cl21 = begin
-                g (f ( fun← an i)) ≡⟨ sym (fiso← cn _)  ⟩
-                fun← cn (fun→ cn (g (f ( fun← an i)))) ≡⟨ cong (fun← cn) eq1 ⟩
-                fun← cn (suc ca) ∎ where open ≡-Reasoning
-         n<ca : (n : ℕ ) → n < count-A (c n)
-         n<ca zero with fun→ cn (g (f (fun← an zero))) | inspect (fun→ cn) (g (f (fun← an zero)))
-         ... | zero | record { eq = eq1 } = cl23 where
-             cl23 : 1 ≤ count-A zero
-             cl23 = ?
-         ... | suc ca | record { eq = eq1 } = cl24 where
-             cl24 : 1 ≤ count-A (suc ca)
-             cl24 = ?
-         n<ca (suc n) with <-cmp (c n) (fun→ cn (g (f (fun← an (suc n)))))
-         ... | tri< ca<an ¬b ¬c = ? where
-             cl26 : n < count-A (c n)
-             cl26 = n<ca n
-             cl25 : suc (suc n) ≤ count-A (fun→ cn (g (f (fun← an (suc n)))))
-             cl25 = begin
-                 suc (suc n) ≤⟨ s≤s (n<ca n) ⟩
-                 suc (count-A (c n)) ≤⟨ s≤s (count-A-mono ( sx≤py→x≤y  ( begin
-                    suc (c n) ≤⟨ ca<an ⟩
-                    fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n)))) ≤⟨ ? ⟩
-                    suc (pred (fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n)))))) ∎ ) ))  ⟩
-                 suc (count-A (pred (fun→ cn (g (f (fun← an (suc n))))))) ≡⟨ ? ⟩
-                 count-A (fun→ cn (g (f (fun← an (suc n))))) ∎ where
-                    open ≤-Reasoning
-         ... | tri≈ ¬a ca=an ¬c = ?
-         ... | tri> ¬a ¬b an<ca = ? where
-             cl25 : suc (suc n) ≤ count-A (max (fun→ cn (g (f (fun← an (suc n))))) (c n))
-             cl25 = ?
-             cl27 : fun→ cn (g (f (fun← an (suc n) )) )  < c (suc n)
-             cl27 = ?
-             cl26 : fun→ cn (g (f (fun← an ? ))  )  < fun→ cn (g (f (fun← an (suc n))))
-             cl26 = ?
-             --
-             --  count-A (c m)                                                           < count (c (suc m))           ≤ count (c n)
-             --  fun→ cn (g (f (fun← an i)))  <  suc (fun→ cn (g (f (fun← an (suc n))))) ≤ fun→ cn (g (f (fun← an j))) ≤ fun→ cn (g (f (fun← an j))) ≡ c n
-             --       c i                                                                 c       (suc i)             c n
-             --  fun→ cn (g (f (fun← an i)))  <  fun→ cn (g (f (fun← an (suc n))))       < fun→ cn (g (f (fun← an j))) ≤ fun→ cn (g (f (fun← an j))) ≡ c n
-             --       c i                             c (suc i)                             c (suc (suc i))             c (suc n)
-             --  count-A (c m) = count-A (c (suc m))  count-A (c (suc m))                  < count (c (suc (suc m))       ≤ count (c (suc n))
+    lem02 n = record { ac = ? ; n<ca = ? }
 
     record CountB (n : ℕ) : Set where
        field