--- a/src/bijection.agda	Sun Jun 11 19:57:52 2023 +0900
+++ b/src/bijection.agda	Sun Jun 11 21:13:55 2023 +0900
@@ -715,8 +715,12 @@
     fla-max (suc n) = max (fun→ cn (g (f (fun← an (suc n))))) (fla-max n)
 
     fla-max< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (fla-max n)
-    fla-max< zero n i≤n = ?
-    fla-max< (suc i) n i≤n = ?
+    fla-max< zero zero (s≤s z≤n) = a<sa 
+    fla-max< (suc i) zero  (s≤s ())
+    fla-max< i (suc n) i≤n with ≤-∨ i≤n
+    ... | case1 refl = s≤s (x≤max  (fun→ cn (g (f (fun← an (suc n))))) (fla-max n))
+    ... | case2 (s≤s (s≤s i<n)) = ≤-trans (fla-max< i n (<-transʳ i<n a<sa)) (s≤s (y≤max (fun→ cn (InjectiveF.f gi (InjectiveF.f fi (fun← an (suc n))))) (fla-max n)))
+
 
     fla0 : (i n : ℕ ) → i < suc n → FList (fla-max n)
     fla0 zero n lt = FLinsert fl0 []  where
@@ -737,11 +741,11 @@
     flany : (n : ℕ) → FLany n
     flany n = record { flist = fla0 n n a<sa ; flany = λ j j<n → flany0 n a<sa j j<n (x<sy→x≤y j<n) } where
         flany0  : (i : ℕ) → (i<n : i < suc n ) → (j : ℕ) → (j<n : j < suc n) → j ≤ i → Any ( ca<n j (fla-max< j n j<n ) ≡_) (fla0 i n i<n)
-        flany0 zero i<n zero j<n z≤n = fl1 where
+        flany0 zero i<n zero j<n z≤n = ? where
             fl0 = ca<n zero (fla-max< zero n 0<s )
             fl1 = x∈FLins fl0 [] 
         flany0 (suc i) (s≤s i<n) j j<n j≤i with ≤-∨ j≤i
-        ... | case1 refl = fl3 where
+        ... | case1 refl = ? where
             fl0 : FL (fla-max n )
             fl0 = ca<n (suc i) (fla-max< (suc i) n (<-transʳ i<n a<sa) )
             fl1 = fla0 i n (≤-trans refl-≤s (s≤s i<n))