--- a/src/bijection.agda	Mon Jun 19 16:01:45 2023 +0900
+++ b/src/bijection.agda	Mon Jun 19 17:57:43 2023 +0900
@@ -610,14 +610,12 @@
            ... | tri≈ ¬a b ¬c = there (nl04 t a)
            ... | tri> ¬a ¬b c₁ = there (nl04 t a)
 
-    n<list : (n : ℕ) → (nl : NL n) → n ≤ length (NL.nlist nl)
-    n<list 0 nl = z≤n
+    n<list : (n : ℕ) → (nl : NL n) → n < length (NL.nlist nl)
+    n<list 0 nl = ?
     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
+    n<list (suc (suc n)) nl = nl03 (suc n) ? ? where
+        nl00 : (n : ℕ ) → (nl : NL (suc n))  → length (NL.nlist (NL-1 _ nl )) < length (NL.nlist nl )
+        nl00 n nl = nl02 n (NL.nlist nl) (NL.anyn nl 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
@@ -627,7 +625,14 @@
            ... | 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)
-     
+        nl03 : (i : ℕ) → i ≤ suc n → (nl : NL i) → suc i < length (NL.nlist nl)
+        nl03 0 i≤sn nl = ?
+        nl03 (suc i) i≤sn nl = begin
+            ? ≤⟨ ? ⟩
+            suc i <⟨ nl03 i ? (NL-1 _ nl ) ⟩
+            length (NL.nlist (NL-1 _ nl )) <⟨ nl00 _ nl ⟩
+            length (NL.nlist nl) ∎  where 
+               open ≤-Reasoning
 
     record maxAC (n : ℕ) : Set where
        field