--- a/FLutil.agda	Mon Sep 14 15:12:32 2020 +0900
+++ b/FLutil.agda	Tue Sep 15 09:00:23 2020 +0900
@@ -202,26 +202,34 @@
 Flist1 (suc i) (s≤s i<n) [] z  = Flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z 
 Flist1 (suc i) i<n (a ∷# x ) z  = FLinsert ((fromℕ< i<n ) :: a ) (Flist1 (suc i) i<n x z )
 
-Flist : {n : ℕ } → FL n → FList n
-Flist {zero} f0 = f0 ∷# [] 
-Flist {suc n} (x :: y)  = Flist1 n a<sa (Flist y) (Flist y)   
-
-FLall1 : (n : ℕ ) → (x : FL (suc n)) → FList (suc n)
-FLall1 zero (zero :: f0) = (zero :: f0) ∷# []
-FLall1 (suc n) (x :: xp) = FLall2 ( FLall1 n xp ) where
-    FLall2 :  (z : FList (suc n)) → FList (suc (suc n))
-    FLall3 : (a : FL (suc n)) → (y : FList (suc n)) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y
-       → fresh (FL (suc (suc n))) ⌊ _f<?_ ⌋ (x :: a) (FLall2 y)
-    FLall2 [] = []
-    FLall2 (cons a y x₁) = cons (x :: a) (FLall2 y) (FLall3 a y x₁)
-    FLall3 a y x₁ = {!!}
-
-FLall : {n : ℕ } → FList n
-FLall {zero} = f0 ∷# []
-FLall {suc n} = FLall1 n fmax 
+∀Flist : {n : ℕ } → FL n → FList n
+∀Flist {zero} f0 = f0 ∷# [] 
+∀Flist {suc n} (x :: y)  = Flist1 n a<sa (∀Flist y) (∀Flist y)   
 
 fr8 : FList 4
-fr8 = Flist (fmax {4}) 
+fr8 = ∀Flist fmax
+
+open import Data.List.Fresh.Relation.Unary.Any 
+
+x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_ ) (FLinsert x xs)
+x∈FLins {zero} f0 [] = here refl
+x∈FLins {zero} f0 (cons f0 xs x) = here refl
+x∈FLins {suc n} x [] = here refl
+x∈FLins {suc n} x (cons a xs x₁) with FLcmp x a
+... | tri< x<a ¬b ¬c = here refl
+... | tri≈ ¬a b ¬c   = here b
+x∈FLins {suc n} x (cons a [] x₁)              | tri> ¬a ¬b a<x = there ( here refl )
+x∈FLins {suc n} x (cons a (cons a₁ xs x₂) x₁) | tri> ¬a ¬b a<x = there ( x∈FLins x (cons a₁ xs x₂) )
+
+x∈∀Flist : {n : ℕ } → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax)
+x∈∀Flist {n} x  = AFlist1 n x where
+    AFlist1 : (n : ℕ ) → (x : FL n)  → Any (_≡_ x) (∀Flist fmax)
+    AFlist1 zero f0 = here refl
+    AFlist1 (suc n) x with FLcmp x fmax 
+    ... | tri< a ¬b ¬c = {!!}
+    ... | tri≈ ¬a refl ¬c = {!!}
+    ... | tri> ¬a ¬b c = ⊥-elim ( fmax< c )
+
 
 -- FLinsert membership
 
@@ -231,17 +239,8 @@
   FL-Setoid  = record { Carrier = FL n ; _≈_ = _≡_ ; isEquivalence = record { sym = sym ; refl = refl ; trans = trans }}
 
   open import Data.List.Fresh.Membership.Setoid FL-Setoid
-  open import Data.List.Fresh.Relation.Unary.Any 
 
   FLinsert-mb :  (x : FL n ) → (xs : FList n)  → x ∈ FLinsert x xs
-  FLinsert-mb x xs = fl1 {n} x xs where
-     fl1 : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_ ) (FLinsert x xs)
-     fl1 {zero} f0 [] = here refl
-     fl1 {zero} f0 (cons f0 xs x) = here refl
-     fl1 {suc n} x [] = here refl
-     fl1 {suc n} x (cons a xs x₁) with FLcmp x a
-     ... | tri< x<a ¬b ¬c = here refl
-     ... | tri≈ ¬a b ¬c   = here b
-     fl1 {suc n} x (cons a [] x₁)              | tri> ¬a ¬b a<x = there ( here refl )
-     fl1 {suc n} x (cons a (cons a₁ xs x₂) x₁) | tri> ¬a ¬b a<x = there ( fl1 x (cons a₁ xs x₂) )
+  FLinsert-mb x xs = x∈FLins {n} x xs 
 
+