--- a/FLutil.agda	Tue Nov 24 11:08:07 2020 +0900
+++ b/FLutil.agda	Tue Nov 24 15:59:42 2020 +0900
@@ -103,12 +103,46 @@
 open import Data.Nat.Properties using ( ≤-trans ; <-trans )
 fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n 
 fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where
-    fsuc2 : toℕ x < toℕ (fromℕ< a<sa) 
-    fsuc2 = lt
     fsuc1 : suc (toℕ x) < n
     fsuc1 =  Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
 fsuc (x :: y) (f<t lt) = x :: fsuc y lt
 
+-- fsuc0 : { n : ℕ } → (x : FL n ) → FL n 
+-- fsuc0 {n} (x :: y) (f<n lt) = fromℕ< fsuc2 :: y where
+--     fsuc2 : suc (toℕ x) < n
+--     fsuc2 =  Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
+-- fsuc0 (x :: y) (f<t lt) = x :: fsuc y lt
+
+open import Data.Maybe
+open import fin
+
+fpredm : { n : ℕ } → (x : FL n ) → Maybe (FL n)
+fpredm f0 = nothing
+fpredm (x :: y) with fpredm y
+... | just y1 = just (x :: y1)
+fpredm (zero :: y) | nothing = nothing
+fpredm (suc x :: y) | nothing = just (fin+1 x :: fmax)
+
+¬<FL0 : {n : ℕ} {y : FL n} → ¬ y f< FL0
+¬<FL0 {suc n} {zero :: y} (f<t lt) = ¬<FL0 {n} {y} lt 
+
+fpred : { n : ℕ } → (x : FL n ) → FL0 f< x  → FL n
+fpred (zero :: y) (f<t lt) = zero :: fpred y lt
+fpred (x :: y) (f<n lt) with FLcmp FL0 y
+... | tri< a ¬b ¬c = x :: fpred y a
+... | tri> ¬a ¬b c = ⊥-elim (¬<FL0 c)
+fpred {suc _} (suc x :: y) (f<n lt) | tri≈ ¬a b ¬c = fin+1 x :: fmax
+
+fpred< : { n : ℕ } → (x : FL n ) → (lt : FL0 f< x ) → fpred x lt f< x
+fpred< (zero :: y) (f<t lt) = f<t (fpred< y lt)
+fpred< (suc x :: y) (f<n lt) with FLcmp FL0 y
+... | tri< a ¬b ¬c = f<t ( fpred< y a)
+... | tri> ¬a ¬b c = ⊥-elim (¬<FL0 c)
+... | tri≈ ¬a refl ¬c = f<n fpr1 where
+   fpr1 : {n : ℕ } {x : Fin n} → fin+1 x Data.Fin.< suc x
+   fpr1 {suc _} {zero} = s≤s z≤n
+   fpr1 {suc _} {suc x} = s≤s fpr1
+
 flist1 :  {n : ℕ } (i : ℕ) → i < suc n → List (FL n) → List (FL n) → List (FL (suc n)) 
 flist1 zero i<n [] _ = []
 flist1 zero i<n (a ∷ x ) z  = ( zero :: a ) ∷ flist1 zero i<n x z 
@@ -123,8 +157,7 @@
 fr22 = refl
 
 fr4 : List (FL 4)
-fr4 = Data.List.reverse (flist (fmax {4}) )
-
+fr4 = Data.List.reverse (flist (fmax {4}) ) 
 -- fr5 : List (List ℕ)
 -- fr5 = map plist (map FL→perm  (Data.List.reverse (flist (fmax {4}) )))
 
@@ -213,9 +246,33 @@
 fr9 : FList 3
 fr9 = ∀Flist fmax
 
+∀Flist' : (n : ℕ ) → FList n
+∀Flist' n = ∀Flist0' n n FL0 {!!} where
+   ∀Flist0' : (i j : ℕ) → (x : FL n) → x f< fmax → FList n
+   ∀Flist0' zero zero x _ = []
+   ∀Flist0' zero (suc j) x lt = ∀Flist0' j j fmax {!!}
+   ∀Flist0' (suc i) j x lt = cons (fsuc x lt) (∀Flist0' i j (fsuc x lt) {!!} ) {!!}
+
+-- 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 = {!!}
+
 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)
+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
 x∈FLins {zero} f0 (cons f0 xs x) = here refl
@@ -230,8 +287,6 @@
 nextAny (here x₁) = there (here x₁)
 nextAny (there any) = there (there any)
 
-open import fin
-
 record ∀FListP (n : ℕ ) : Set (Level.suc Level.zero) where
   field
     ∀list :   FList n