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

diff -r 16ad3c7aa287 -r 0f3cb18beebf FLutil.agda
--- a/FLutil.agda	Mon Nov 23 08:33:06 2020 +0900
+++ b/FLutil.agda	Mon Nov 23 09:20:38 2020 +0900
@@ -234,29 +234,26 @@
 ∀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) = 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
     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 n) → fresh (FL n) ⌊ _f<?_ ⌋ a y 
-        → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< i<n :: a) y1 →  FList (suc n)
-    af4 zero i<n [] y1 a fr0 fr = y1
-    af4 zero (s≤s i<n) (cons a' y x) y1 a (lift a<a' , q) fr =
-      af4 zero 0<s y (cons (zero :: a') y1 (af41 a fr {!!})) a' {!!} ({!!} , af41 a fr {!!} ) where 
-       af41 : (a : FL n) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (zero :: a) y1 → a' f< a  → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (zero :: a') y1
-       af41 a fr lt = ttf (f<t lt) y1 fr
-    af4 (suc i) (s≤s i<n) [] y1 a fr0 fr = af4 i (≤-trans i<n a≤sa) (∀FListP.∀list af0) y1 fmax {!!} (af42 fr) where
-       af42 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a) y1 → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (≤-trans i<n a≤sa) :: fmax) y1
+        → (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 (lift a<a' , q) fr =
-      af4 (suc i) (s≤s i<n) y (cons (fromℕ< (s≤s i<n) :: a') y1 {!!}) a' {!!} ({!!} , {!!} ) where -- 
-       af43 : (a : FL n) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a) y1 → a' f< a
-          → fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a') y1
-       af43 a fr lt = ttf (f<t lt) y1 fr
+    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 = {!!}