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

diff -r 17c19100ecfd -r d69252685ed9 FLutil.agda
--- a/FLutil.agda	Mon Nov 23 11:09:44 2020 +0900
+++ b/FLutil.agda	Mon Nov 23 12:13:02 2020 +0900
@@ -246,7 +246,17 @@
     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 i i<n y a fr y1 fr1 = {!!}
+    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 = {!!}
 
 
 -- FLinsert membership