--- a/FLutil.agda	Wed Nov 25 23:28:51 2020 +0900
+++ b/FLutil.agda	Thu Nov 26 00:30:05 2020 +0900
@@ -230,60 +230,30 @@
 -- open import Data.List.Fresh.Relation.Unary.All
 -- fr7 = append ( ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# [] ) fr1 ( ({!!} , {!!} ) ∷ [] )
 
-Flist1 :  {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n)
-Flist1 zero i<n [] _ = []
-Flist1 zero i<n (a ∷# x ) z  = FLinsert ( zero :: a ) (Flist1 zero i<n x z )
-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 : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n)
+Flist zero i<n [] _ = []
+Flist zero i<n (a ∷# x ) z  = FLinsert ( zero :: a ) (Flist zero i<n x z )
+Flist (suc i) (s≤s i<n) [] z  = Flist i (Data.Nat.Properties.<-trans i<n a<sa) z z 
+Flist (suc i) i<n (a ∷# x ) z  = FLinsert ((fromℕ< i<n ) :: a ) (Flist (suc i) i<n x z )
 
-∀FlistI : {n : ℕ } → FL n → FList n
-∀FlistI {zero} f0 = f0 ∷# [] 
-∀FlistI {suc n} (x :: y)  = Flist1 n a<sa (∀FlistI y) (∀FlistI y)   
+∀Flist : {n : ℕ } → FL n → FList n
+∀Flist {zero} f0 = f0 ∷# [] 
+∀Flist {suc n} (x :: y)  = Flist n a<sa (∀Flist y) (∀Flist 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 refl ¬c = cons FL0 L xr
-... | 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 [] (Level.lift tt)
+fr8 = ∀Flist fmax 
 
 fr9 : FList 3
-fr9 = ∀Flist fmax [] (Level.lift tt)
+fr9 = ∀Flist fmax 
 
 open import Data.List.Fresh.Relation.Unary.Any 
 open import Data.List.Fresh.Relation.Unary.All 
 
-AnyFList0 : {n : ℕ} (x : FL n ) → (L : FList n ) → (fr : fresh (FL n) ⌊ _f<?_ ⌋ x L ) → Any (x ≡_ ) (∀Flist x L fr)
-AnyFList0 x L fr with FLcmp x FL0
-... | tri< a ¬b ¬c = ⊥-elim (¬x<FL0 a)
-... | tri≈ ¬a refl ¬c = here refl
-AnyFList0 {n} x L xr | tri> ¬a ¬b c = af0 x L c xr (here refl) where
-   af0 : (y : FL n) → (L : FList n) → (c : FL0 f< y) → (yr : fresh (FL n) ⌊ _f<?_ ⌋ y L ) →  Any (x ≡_ ) (cons y L yr)
-       → Any (x ≡_ ) (∀Flist (fpred y c) (cons y L yr) ( Level.lift (fromWitness (fpred< y c)) , ttf (fpred< y c) L yr)) 
-   af0 y L c yr any with FLcmp (fpred y c) FL0
-   ... | tri< a ¬b ¬c = ⊥-elim (¬x<FL0 a)
-   ... | tri≈ ¬a b ¬c = subst (λ k → Any (x ≡_ ) k) {!!} (there any)
-   ... | tri> ¬a ¬b c₁ = {!!}
-
-{-# TERMINATING #-}
-AnyFList : {n : ℕ }  → (x : FL (suc n) ) →  Any (x ≡_ ) (∀Flist fmax [] (Level.lift tt))
-AnyFList {n} x with FLcmp x fmax
-... | tri> ¬a ¬b c = ⊥-elim (fmax< c)
-... | tri≈ ¬a refl ¬c = AnyFList0 x [] (Level.lift tt)
-... | tri< a ¬b ¬c = AnyFList1 fmax x a [] (Level.lift tt) where
-   AnyFList1 : {n : ℕ} (x y : FL n ) → y f< x  → (L : FList n ) → (fr : fresh (FL n) ⌊ _f<?_ ⌋ x L ) → Any (y ≡_ ) (∀Flist x L fr)
-   AnyFList1 x y y<x L fr with FLcmp x FL0
-   ... | tri< a ¬b ¬c = ⊥-elim (¬x<FL0 a)
-   ... | tri≈ ¬a refl ¬c = ⊥-elim (¬x<FL0 y<x)
-   ... | tri> ¬a ¬b c = af1 where
-        af1 : Any (_≡_ y) (∀Flist (fpred x c)  (cons x L fr)  ( Level.lift (fromWitness (fpred< x c)) , ttf (fpred< x c) L fr) ) 
-        af1 = {!!}
+AnyFList : {n : ℕ }  → (x : FL (suc n) ) →  Any (x ≡_ ) (∀Flist fmax)
+AnyFList {n} = {!!}
 
 x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_ ) (FLinsert x xs)
 x∈FLins {zero} f0 [] = here refl