# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1606348692 -32400
# Node ID 7423f0fc124ad122dc1dd31a324b3a460ca2e85f
# Parent  d631469259f28b5f5b70d209cde66ffbd0313b9a
... almost ...

diff -r d631469259f2 -r 7423f0fc124a FLutil.agda
--- a/FLutil.agda	Thu Nov 26 08:10:06 2020 +0900
+++ b/FLutil.agda	Thu Nov 26 08:58:12 2020 +0900
@@ -234,22 +234,20 @@
 Ffresh0 : {n : ℕ } → (i<n : zero < suc n) → (a : FL n) → (x z : FList n )
     →  fresh (FL n) ⌊ _f<?_ ⌋ a x →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ (zero :: a) (Flist zero i<n x z)
 Ffresh1 : {n : ℕ } → (i : ℕ) → (i<n : i < suc n) → 0 < i → (a : FL n) → (x z : FList n )
-    →  fresh (FL n) ⌊ _f<?_ ⌋ a x →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) (Flist i i<n x z)
+     →  (a₂ : FL (suc n)) (t : FList (suc n)) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a₂ t 
+     →  fresh (FL n) ⌊ _f<?_ ⌋ a x →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) t
 Flist zero i<n [] _ = []
 Flist zero i<n (cons a x xr) z  = cons ( zero :: a ) (Flist zero i<n x z ) (Ffresh0 i<n a x z xr)
 Flist (suc i) (s≤s i<n) [] z  = Flist i (<-trans i<n a<sa) z z 
-Flist (suc i) i<n (cons a x xr) z  = cons ((fromℕ< i<n ) :: a ) (Flist (suc i) i<n x z ) (Ffresh1 (suc i) i<n 0<s a x z xr)
+Flist (suc i) (s≤s i<n) (cons a [] xr) z = cons ((fromℕ< (s≤s i<n)) :: a) (Flist i (<-trans i<n a<sa) z z)  {!!}
+Flist (suc i) (s≤s i<n) (cons a (cons a₁ x x₁) xr) z with Flist (suc i) (s≤s i<n) x z 
+... | [] = cons ((fromℕ< (s≤s i<n)) :: a) [] (Level.lift tt)
+... | cons a₂ t x₂ = cons ((fromℕ< (s≤s i<n)) :: a) t (Ffresh1 (suc i) (s≤s i<n) 0<s a x z a₂ t x₂ ?)
 Ffresh0 i<n a [] z xr = Level.lift tt
 Ffresh0 i<n a (cons a₁ x x₁) z (lift a<a₁ , ar) = Fr0 , Ffresh0 i<n a x z ar where
    Fr0 : ⌊ _f<?_ ⌋ (zero :: a) (zero :: a₁)
    Fr0 = Level.lift (fromWitness (f<t (toWitness a<a₁)))
-Ffresh1 zero i<n () a [] z xr 
-Ffresh1 (suc i) (s≤s i<n) a _ [] z (Level.lift tt) with Flist i (<-trans i<n a<sa) z z 
-... | [] = Level.lift tt
-... | cons a₁ t x = {!!} , ttf {!!} t x
-Ffresh1 zero i<n () a (cons a₁ x xr) z (a<a₁ , ar) 
-Ffresh1 {n} (suc i) i<n _ a (cons a₁ x xr) z (a<a₁ , ar) with Ffresh1 {n} (suc i) i<n 0<s a x z ar  --  (suc (fromℕ< (≤-pred i<n)) :: a) (Flist (suc i) i<n x z)
-... | t = {!!} -- (suc (fromℕ< (≤-pred i<n)) :: a) (Flist (suc i) i<n (cons a₁ x xr) z)
+Ffresh1 = {!!}
 
 ∀Flist : {n : ℕ } → FL n → FList n
 ∀Flist {zero} f0 = f0 ∷# []