--- a/FLComm.agda	Tue Dec 08 11:05:22 2020 +0900
+++ b/FLComm.agda	Tue Dec 08 11:46:49 2020 +0900
@@ -46,45 +46,29 @@
 -- ∀Flist {zero} f0 = f0 ∷# [] 
 -- Flist {suc n} (x :: y)  = Flist n a<sa (∀Flist y) (∀Flist y)   
 
+-------------
+--    (suc n :: (fromℕ< a<sa  :: p))   (n ::  ) ....           (zero :: (fromℕ< a<sa :: p))
+--    (suc n :: (n :: p)
+--           :                     anyFL
+--    (suc n :: (zero :: p)
+
 -- all FL
-record AnyFL (n : ℕ) (p : FL n) : Set where
+record AnyFL {i : ℕ} (i<n : i < suc n) : Set where
    field
-     anyList : FList n
-     anyP : (x : FL n) → p f≤ x →  Any (x ≡_ ) anyList 
+     anyList : FList (suc n)
+     anyP : (x : FL n) → Any (fromℕ< i<n  :: x ≡_ ) anyList 
 
 open import fin
 open AnyFL
-anyFL : (n : ℕ ) → AnyFL n FL0
-anyFL zero = record { anyList =  f0 ∷# []  ; anyP = any00 } where
-   any00 : (p : FL zero) →  FL0 f≤ p → Any (p ≡_) (f0 ∷# [])
-   any00 f0 (case1 refl) = here refl
-anyFL (suc n) = any01 n (anyList (anyFL n)) (anyP (anyFL n) FL0 (case1 refl) ) {!!} where
-   -- any03 : AnyFL (suc n) (fromℕ< a<sa :: fmax) → AnyFL (suc n) FL0
-   -- loop on i 
-   any02 : (i : ℕ ) → (i<n : i < suc n ) → (a : FL n) → AnyFL (suc n) (fromℕ< i<n  :: a) → AnyFL (suc n) (zero :: a)
-   any02 zero (s≤s z≤n) a any = any
-   any02 (suc i) (s≤s i<n) a any = any02 i (<-trans i<n a<sa) a record { anyList = cons ((fromℕ< (s≤s i<n )) :: a) (anyList any) any07 ; anyP = any08 } where
-      any07 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a) (anyList any)
-      any07 = {!!}
-      any08 : (x : FL (suc n)) → (fromℕ< (<-trans i<n a<sa) :: a) f≤ x → Any (x ≡_) (cons (fromℕ< (s≤s i<n) :: a) (anyList any) any07 )
-      any08 = {!!}
-   -- loop on a 
-   any03 :  (L : FList n) → (a : FL n) →  fresh (FL n) ⌊ _f<?_ ⌋ a L  →  AnyFL (suc n) (fromℕ< a<sa :: a ) → AnyFL (suc n) FL0
-   any03 [] a ar any = {!!} -- any02 n a<sa a any
-   any03 (cons b L br) a ( Data.Product._,_ (Level.lift a<b)_) any = any03 L b br record { anyList = anyList any04 ; anyP = any05 } where
-      any04 : AnyFL (suc n) (zero :: a)
-      any04 = any02 n a<sa a any
-      any05 : (x : FL (suc n)) → (fromℕ< a<sa :: b) f≤ x → Any (x ≡_) (anyList any04) -- 0<fmax : zero Data.Fin.< fromℕ< a<sa
-      any05 x mb≤x  = anyP any04 x (any06 a b x (toWitness a<b) mb≤x) where
-         any06 : {n : ℕ } → (a b : FL n) → (x : FL (suc n)) → a f< b → (fromℕ< {n} a<sa :: b) f≤ x → (zero :: a) f≤ x 
-         any06 {suc n} a b x a<b (case1 refl) = case2 (f<n 0<fmax)
-         any06 {suc n} a b x a<b (case2 mb<x) = case2 (f<-trans (f<n 0<fmax) mb<x) 
-   any01 : (i : ℕ ) → (L : FList n) → Any (FL0 ≡_) L → AnyFL (suc n) fmax → AnyFL (suc n) FL0 
-   any01 zero [] ()
-   any01 (suc i) [] ()
-   any01 zero (cons a L x)    _ any = {!!}
-   any01 (suc i) (cons .FL0 L x) (here refl) any = any01 i L {!!} {!!} -- can't happen
-   any01 (suc i) (cons a L ar) (there b) any = any03 L a ar {!!}
+anyFL :  AnyFL a<sa
+anyFL = record { anyList = FLinsert (fromℕ< a<sa :: fmax ) (anyListF fin<n) ; anyP = {!!} }  where
+  anyListFL : (P1 : FL n) → FList (suc n)
+  anyListFL (zero :: _)  = anyList anyFL 
+  anyListFL (suc p :: P1) =  FLinsert (fromℕ< a<sa  :: (suc p :: P1)) (anyListFL (fin+1 p :: P1))
+  anyListF : {i : ℕ} → (Q1 : i < suc n) → FList (suc n)
+  anyListF (s≤s z≤n) = anyListFL fmax
+  anyListF (s≤s (s≤s i<n)) = {!!} --FLinsert (fromℕ< (s≤s i<n) :: fmax) ? -- (anyListF (s≤s i<n) fmax)
+  
 
 tl3 : (FL n) → ( z : FList n) → FList n → FList n
 tl3 h [] w = w
@@ -100,7 +84,7 @@
 CommFListN  0 = ∀Flist fmax
 CommFListN  (suc i) = CommFList (CommFListN i)
 
--- all comm cobmbination in P and Q
+-- all cobmbination in P and Q
 record AnyComm  (P Q : FList n) (fpq : (p q : FL n) → FL n) : Set where
    field
      commList : FList n