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

diff -r 0f3cb18beebf -r 17c19100ecfd FLutil.agda
--- a/FLutil.agda	Mon Nov 23 09:20:38 2020 +0900
+++ b/FLutil.agda	Mon Nov 23 11:09:44 2020 +0900
@@ -234,28 +234,19 @@
 ∀FList zero = record { ∀list = f0 ∷# [] ; x∈∀list = af1 } where
     af1 : (x : FL zero) → Any  (_≡_ x) (cons f0 [] (Level.lift tt))
     af1 f0 = here refl
-∀FList (suc n) = record { ∀list = af4 n ≤-refl (∀FListP.∀list af0) [] fmax (Level.lift tt)
-       ; x∈∀list = λ x → af2 x  ( af4 n ≤-refl (∀FListP.∀list af0) [] fmax (Level.lift tt)) } where
+∀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)
+       ; x∈∀list = λ x → {!!} } where
     af0 : ∀FListP n
     af0 = ∀FList n
     af3 : (w : Fin (suc n)) (x y : FL n) → Level.Lift Level.zero (True (x f<? y )) → (w :: x ) f< (w :: y )
     af3 w x y (Level.lift z) with x f<? y
     ... | yes x<y = f<t x<y
-    af4  : (i : ℕ) → (i<n : i < suc n) → ( y : FList n ) → (y1 : FList (suc n))
-        → (a : FL (suc n)) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y1 →  FList (suc n)
-    af4 zero i<n [] y1 a fr = y1
-    af4 zero (s≤s i<n) (cons a' y x) y1 a fr =
-      af4 zero 0<s y (cons a y1 fr) (zero :: a') ({!!} , af41 x) where  -- x : freash a' y, fr : fresh a y1
-       af41 : fresh (FL n) ⌊ _f<?_ ⌋ a' y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (zero :: a') y1
-       af41 = {!!}
-    af4 (suc i) (s≤s i<n) [] y1 a fr = af4 i (≤-trans i<n a≤sa) (∀FListP.∀list af0) y1 fmax (af42 fr) where
-       af42 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y1 → fresh (FL (suc n)) ⌊ _f<?_ ⌋ fmax y1
-       af42 = {!!}
-    af4 (suc i) (s≤s i<n) (cons a' y x) y1 a fr = af4 (suc i) (s≤s i<n) y (cons a y1 fr) (fromℕ< (s≤s i<n) :: a') ({!!} , af43 fr) where -- 
-       af43 :  fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y1 → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a') y1
-       af43 fr  = {!!}
-    af2 : (x : FL (suc n)) → (y : FList (suc n)) → Any (_≡_ x) y
-    af2 = {!!}
+    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 = {!!}
 
 
 -- FLinsert membership