# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1606121908 -32400
# Node ID 53d31ba08456bbcad95a1870c72675f2290b2c41
# Parent  d69252685ed984c613d272f0dbf5f33580ca860e
... ?

diff -r d69252685ed9 -r 53d31ba08456 FLutil.agda
--- a/FLutil.agda	Mon Nov 23 12:13:02 2020 +0900
+++ b/FLutil.agda	Mon Nov 23 17:58:28 2020 +0900
@@ -236,7 +236,7 @@
     af1 f0 = here refl
 ∀FList (suc n) with ∀FListP.∀list (∀FList n) | ∀FListP.x∈∀list (∀FList n) fmax
 ∀FList (suc n) | [] | ()
-∀FList (suc n) | cons a y fr | _ = record { ∀list = af4 n ≤-refl a y fr [] (Level.lift tt)
+∀FList (suc n) | cons a x fr | _ = record { ∀list = af4 n ≤-refl a x fr
        ; x∈∀list = λ x → {!!} } where
     af0 : ∀FListP n
     af0 = ∀FList n
@@ -245,19 +245,20 @@
     ... | yes x<y = f<t x<y
     af4  : (i : ℕ) → (i<n : i < suc n) 
         → (a : FL n) → (y : FList n) → fresh (FL n) ⌊ _f<?_ ⌋ a y  
-        → (y1 : FList (suc n)) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) y1  →  FList (suc n)
-    af4 zero i<n a [] fr y1 fr1 = cons (fromℕ< i<n :: a) y1 fr1
-    --  a < a₁
-    af4 zero i<n a (cons a₁ y x) (lift p , fr) y1 fr1 = af4 zero i<n a₁ y x (cons (fromℕ< i<n :: a) y1 fr1) {!!} where
-        af41 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) (cons (fromℕ< i<n :: a₁) y1 {!!})
-        af41 = Level.lift (fromWitness (f<t {!!})) , ttf {!!} y1 fr1
-    af4 (suc i) (s≤s i<n) a' [] fr' y1 fr1 = af4 i (<-trans i<n a<sa) a y fr y1 af42 where
-        af42 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (<-trans i<n a<sa) :: a) y1
-        af42 = {!!}
-    af4 (suc i) (s≤s i<n) a (cons a₁ y x) (lift p , fr) y1 fr1 = af4 (suc i) (s≤s i<n) a₁ y x (cons  (fromℕ< (s≤s i<n) :: a) y1 fr1) af43 where
-        af43 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a₁) (cons (fromℕ< (s≤s i<n) :: a) y1 fr1)
-        af43 = {!!}
-
+        →  FList (suc n)
+    af4r  : (i : ℕ) → (i<n : i < suc n) 
+        → (a : FL n) → (y : FList n) → (fr : fresh (FL n) ⌊ _f<?_ ⌋ a y )
+        →  fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) (af4 i i<n a y fr)
+    af4 zero i<n a [] fr = cons (fromℕ< i<n :: a) [] (Level.lift tt)
+    af4 zero i<n a (cons a₁ y x) (lift p , fr) =
+        cons (fromℕ< i<n :: a) ( af4 zero i<n a₁ y x ) (ttf (f<t (toWitness p)) ( af4 zero i<n a₁ y x ) (af4r zero i<n a₁ y x))
+    af4 (suc i) (s≤s i<n) a' [] fr' = af4 i (<-trans i<n a<sa) a x fr
+    af4 (suc i) (s≤s i<n) a (cons a₁ y x) (lift p , fr) = 
+        cons  (fromℕ< (s≤s i<n) :: a₁) ( af4 (suc i) (s≤s i<n) a₁ y x ) ( af4r (suc i) (s≤s i<n) a₁ y x )
+    af4r zero i<n a [] fr =  {!!} , Level.lift tt
+    af4r zero i<n a (cons a₁ y x) fr = {!!} , {!!}
+    af4r (suc i) i<n a [] fr = {!!}
+    af4r (suc i) i<n a (cons a₁ y x) fr = {!!}
 
 -- FLinsert membership