--- a/FLutil.agda	Tue Sep 15 09:25:45 2020 +0900
+++ b/FLutil.agda	Fri Sep 18 09:48:13 2020 +0900
@@ -3,9 +3,10 @@
 
 open import Level hiding ( suc ; zero )
 open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ ; _≟_)
-open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
+open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
 open import Data.Fin.Permutation
 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
+open import Data.Nat.Properties
 open import Relation.Binary.PropositionalEquality 
 open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev )
 open import Data.Product
@@ -147,7 +148,7 @@
 
 open import Data.Product
 open import Relation.Nullary.Decidable hiding (⌊_⌋)
-open import Data.Bool hiding (_<_)
+open import Data.Bool hiding (_<_ ; _≤_ )
 open import Data.Unit.Base using (⊤ ; tt)
 
 --  fresh a []        = ⊤
@@ -210,6 +211,7 @@
 fr8 = ∀Flist fmax
 
 open import Data.List.Fresh.Relation.Unary.Any 
+open import Data.List.Fresh.Relation.Unary.All 
 
 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_ ) (FLinsert x xs)
 x∈FLins {zero} f0 [] = here refl
@@ -223,18 +225,31 @@
 
 open import fin
 
-x∈∀Flist : {n : ℕ } → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax)
-x∈∀Flist {n} x  = AFlist1 n x where
-    AFList0 : (n : ℕ ) →  Any (_≡_ (fromℕ< a<sa :: fmax)) (Flist1 n a<sa (∀Flist fmax) (∀Flist fmax))
-    AFList0 = {!!}
-    AFList2 : (n : ℕ )  (x : FL (suc n)) → (x1 : Fin (suc n)) (y : FL n) → x f< ( x1 :: y)  → Any (_≡_ x) (Flist1 n a<sa (∀Flist y) (∀Flist y))
-    AFList2 = {!!}
-    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 = AFList2 n x (fromℕ< a<sa) (fmax {n}) (fmax¬ ¬b)
-    ... | tri≈ ¬a refl ¬c = AFList0 n
-    ... | tri> ¬a ¬b c = ⊥-elim ( fmax< c )
+record ∀FListP (n : ℕ ) : Set (Level.suc Level.zero) where
+  field
+    ∀list :   FList n 
+    x∈∀list : (x : FL n ) → Any (x ≡_ ) ∀list 
+
+∀FList : (n : ℕ )  → ∀FListP n
+∀FList zero = record { ∀list = f0 ∷# [] ; x∈∀list = af1 } where
+    af1 : (x : FL zero) → Any  (_≡_ x) (cons f0 [] (Level.lift tt))
+    af1 f0 = here refl
+∀FList (suc n) = record { ∀list = af1 (suc n) ≤-refl ; x∈∀list = λ x → af2 x (af1 (suc n) ≤-refl ) } where
+    af0 : ∀FListP n
+    af0 = ∀FList n
+    af3 : (w : Fin (suc n)) (x y : FL n) → Level.Lift Level.zero (True (x f<? y )) → (w :: x ) f< (w :: y )
+    af3 w x y (Level.lift z) with x f<? y
+    ... | yes x<y = f<t x<y
+    af1 : (i : ℕ ) → i ≤ suc n  → FList (suc n)
+    af4 : (i : ℕ ) → (i<n : i ≤ n) → All {_} {_} {_} {_} {⌊ _f<?_ ⌋} (_# af1 i (≤-trans i<n a≤sa)) (Data.List.Fresh.map (fromℕ< (s≤s i<n) ::_)
+     (λ {x} {x₁} xr → Level.lift (fromWitness (af3 (fromℕ< (s≤s i<n)) x x₁ xr))) (∀FListP.∀list af0))
+    af4 = {!!}
+    af1 zero i<n  = Data.List.Fresh.map (zero ::_ ) (λ {x} {x₁} xr → Level.lift (fromWitness (af3 zero x x₁ xr ) )) (∀FListP.∀list af0 )
+    af1 (suc i) (s≤s i<n) = append (Data.List.Fresh.map (fromℕ< (s≤s i<n) ::_ )
+             (λ {x} {x₁} xr → Level.lift (fromWitness (af3 (fromℕ< (s≤s i<n)) x x₁ xr ) )) (∀FListP.∀list af0 ))
+       (af1 i (≤-trans i<n a≤sa)) (af4 i i<n )
+    af2 : (x : FL (suc n)) → (y : FList (suc n)) → Any (_≡_ x) y
+    af2 = {!!}
 
 
 -- FLinsert membership