# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607121151 -32400
# Node ID 40695d752dd0e004ffa1dbf2592181f8fa6a86af
# Parent  47df9343efa944abb1d25fb26c965fd3a7d3a2a3
...

diff -r 47df9343efa9 -r 40695d752dd0 FLComm.agda
--- a/FLComm.agda	Fri Dec 04 22:47:01 2020 +0900
+++ b/FLComm.agda	Sat Dec 05 07:32:31 2020 +0900
@@ -55,18 +55,18 @@
 anyFL zero = record { anyList =  f0 ∷# []  ; anyP = any00 } where
    any00 : (p : FL zero) →  FL0 f≤ p → Any (_≡ p) (f0 ∷# [])
    any00 f0 (case1 refl) = here refl
-anyFL (suc n) = any01 n (anyList (anyFL n)) (anyP (anyFL n) FL0 (case1 refl) ) {!!} where
+anyFL (suc n) = any01 n (anyList (anyFL n)) (anyP (anyFL n) FL0 (case1 refl) ) fmax {!!} where
    any02 : (i : ℕ ) → (i<n : i < suc n ) → (a : FL n) → AnyFL (suc n) (fromℕ< i<n  :: a) → AnyFL (suc n) (zero :: a)
    any02 zero (s≤s z≤n) a any = any
    any02 (suc i) i<n a any = {!!}
-   any01 : (i : ℕ ) → (L : FList n) → Any (_≡ FL0) L → AnyFL (suc n) fmax → AnyFL (suc n) FL0 
-   any01 zero [] ()
-   any01 (suc i) [] ()
-   any01 zero (cons a L x)    _ any = any03 any where
+   any01 : (i : ℕ ) → (L : FList n) → Any (_≡ FL0) L → (x : FL (suc n)) → AnyFL (suc n) x → AnyFL (suc n) FL0 
+   any01 zero [] _ x any = {!!}
+   any01 (suc i) [] _ x any = {!!}
+   any01 zero (cons a L x)    _ y any = any03 {!!} where
       any03 : AnyFL (suc n) (fromℕ< a<sa :: fmax) → AnyFL (suc n) FL0
       any03 any = any02 n a<sa FL0 {!!}
-   any01 (suc i) (cons .FL0 L x) (here refl) any = any01 i L {!!} {!!} -- can't happen
-   any01 (suc i) (cons a L x) (there b) any = any01 i L b any 
+   any01 (suc i) (cons .FL0 L x) (here refl) y any = any01 i L {!!} {!!} {!!} -- can't happen
+   any01 (suc i) (cons a L x) (there b) y any = {!!} -- any01 i L b any 
 
 -- all comm cobmbibation in P and Q
 record AnyComm (P Q : FList n) : Set where