--- a/FLutil.agda	Wed Nov 25 06:15:09 2020 +0900
+++ b/FLutil.agda	Wed Nov 25 07:18:05 2020 +0900
@@ -193,7 +193,7 @@
 -- ... | yes y = subst (λ k → Data.Bool.T k ) refl tt
 -- ... | no nn = ⊥-elim ( nn x<a )
 
-ttf : {n : ℕ } {x a : FL (suc n)} → x f< a → (y : FList (suc n)) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
+ttf : {n : ℕ } {x a : FL (n)} → x f< a → (y : FList (n)) →  fresh (FL (n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (n)) ⌊ _f<?_ ⌋  x y
 ttf _ [] fr = Level.lift tt
 ttf {_} {x} {a} lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf (ttf1 lt1 lt) y x1 where 
        ttf1 : True (a f<? a₁) → x f< a  → x f< a₁
@@ -236,45 +236,32 @@
 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)   
+∀FlistI : {n : ℕ } → FL n → FList n
+∀FlistI {zero} f0 = f0 ∷# [] 
+∀FlistI {suc n} (x :: y)  = Flist1 n a<sa (∀FlistI y) (∀FlistI y)   
+
+¬x<FL0 : {n : ℕ} {x : FL n} → ¬ ( x f< FL0 )
+¬x<FL0 {suc n} {zero :: y} (f<t not) = ¬x<FL0 {n} {y} not
+
+{-# TERMINATING #-}
+∀Flist : {n : ℕ } → (x : FL n ) → (L : FList n ) → fresh (FL n) ⌊ _f<?_ ⌋ x L → FList n 
+∀Flist x L xr with FLcmp x FL0
+... | tri< a ¬b ¬c = ⊥-elim (¬x<FL0 a)
+... | tri≈ ¬a b ¬c = L
+... | tri> ¬a ¬b c = ∀Flist (fpred x c) (cons x L xr) ( Level.lift (fromWitness (fpred< x c)) , ttf (fpred< x c) L xr) 
 
 fr8 : FList 4
-fr8 = ∀Flist fmax
+fr8 = ∀Flist fmax [] (Level.lift tt)
 
 fr9 : FList 3
-fr9 = ∀Flist fmax
-
-∀F1 : {n : ℕ } → FL (suc n) → Fin n → FList (suc n) → FList (suc n)
-∀F1 _ _ [] L = L
-∀F1 y (cons x t xr) L = ∀F1 y t (cons (fin+1 y :: x) L ? )
-
-∀Flist' : (n : ℕ ) → FL n  → FList n → FList n
-∀Flist' zero f0 L = L
-∀Flist' (suc n) (zero :: y) L = ∀F1 zero (∀Flist' n []) L
-∀Flist' (suc n) (suc x :: y) L = 
-    ∀Flist' (suc n) (x :: y) ( ∀F1 (suc x) ( ∀Flist' n y []) L )
-
--- open import Size
--- 
--- record  CFresh {n : ℕ } (i : Size) : Set  where
---    coinductive
---    field
---       δ : ∀{j : Size< i} → (y : FL n) → CFresh {n} j 
---       -- δ : ∀{j : Size< i} → (y : FL n) → (xr : fresh (FL n) ⌊ _f<?_ ⌋ y x) → CFresh {n} j (cons y x xr)
--- 
--- open CFresh
--- 
--- ∀CF : ∀{i} {n : ℕ } → FL n → CFresh {n} i ?
--- δ (∀CF x) y fr = {!!}
+fr9 = ∀Flist fmax [] (Level.lift tt)
 
 open import Data.List.Fresh.Relation.Unary.Any 
 open import Data.List.Fresh.Relation.Unary.All 
 
-AnyFList' : (n : ℕ )  → (x : FL n ) →  Any (x ≡_ ) {!!} -- (∀Flist' n fmax)
-AnyFList' 0 f0 = {!!}
-AnyFList' (suc n) (x :: y) = {!!}
+AnyFList : (n : ℕ )  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax [] (Level.lift tt))
+AnyFList 0 f0 = ?
+AnyFList (suc n) (x :: y) = {!!}
 
 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_ ) (FLinsert x xs)
 x∈FLins {zero} f0 [] = here refl
@@ -297,27 +284,6 @@
 
 open ∀FListP
 
--- open import Data.Fin.Properties as FinP
-
-AnyFList : (n : ℕ )  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax)
-AnyFList n x = AnyFlist0 fmax x where
-   AnyFlist1 :  {n : ℕ } (i : ℕ) → (i<n : i < suc n ) → (x : Fin (suc n)) → (y : FL n) → toℕ x < suc i → (L L1 : FList n )
-       → Any (y ≡_ ) L1 → Any (y ≡_ ) L →  Any ((x :: y ) ≡_ ) (Flist1 i i<n L L1 )
-   AnyFlist1 zero i<n zero y (s≤s x<i) (cons _ L _) L1 any (here refl) = x∈FLins (zero :: y) (Flist1 zero i<n L L1 )
-   AnyFlist1 zero i<n zero y (s≤s x<i) (cons a L ar) L1 any (there any0) = anf0 (AnyFlist1 zero i<n zero y (s≤s x<i) L L1 any any0) where
-        anf0 :  Any ((zero :: y ) ≡_ ) (Flist1 zero i<n L L1) → Any (_≡_ (zero :: y)) (Flist1 zero i<n (cons a L ar) L1)
-        anf0 = {!!}
-   AnyFlist1 (suc i) i<n x y x<i (cons y L ar) L1 any (here refl) with <-fcmp x (fromℕ< i<n)
-   ... | tri≈ ¬a refl ¬c = subst {!!} {!!} (x∈FLins (x :: y) (Flist1 (suc i) i<n L L1 ))
-   ... | tri> ¬a ¬b c = {!!}
-   ... | tri< a ¬b ¬c with AnyFlist1 i {!!} x y {!!} L1 L1 any any 
-   ... | t = {!!}
-   AnyFlist1 (suc i) i<n x y x<i (cons a L ar) L1 any (there any0) with AnyFlist1 (suc i) i<n x y x<i L L1 any any0
-   ... | t = {!!}
-   AnyFlist0 : {n : ℕ } → (y x : FL n ) →  Any (x ≡_ ) (∀Flist y)
-   AnyFlist0 {zero} f0 f0 = here refl
-   AnyFlist0 {suc n} (_ :: z) (x :: y) = AnyFlist1 n a<sa x y fin<n (∀Flist z) (∀Flist z) (AnyFlist0 z y) (AnyFlist0 z y)
-
 -- tt1 : FList 3
 -- tt1 = ∀FListP.∀list (∀FList 3)