# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595266749 -32400
# Node ID 0a116938a564c0ebe8042a9fcc7873765fd7356c
# Parent  7b6592f0851ab0fd56fa8a4062a64041729696ff
...

diff -r 7b6592f0851a -r 0a116938a564 filter.agda
--- a/filter.agda	Tue Jul 21 02:19:07 2020 +0900
+++ b/filter.agda	Tue Jul 21 02:39:09 2020 +0900
@@ -219,11 +219,15 @@
      find (j0 ∷ _) 0 v0 = i0
      find (j1 ∷ _) 0 v1 = i1
      find (d ∷ n) (Suc x) (vn {n} {d} {x} p) = find n x p 
+     lemma : (h : Three) → (n : List Three) → {x : Nat} {p : Findp n x } → find n x p ≡ find (h ∷ n) (Suc x) (vn p)
+     lemma j0 n {x} {p} = refl
+     lemma j1 n {x} {p} = refl
+     lemma j2 n {x} {p} = refl
      feq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q
      feq n {0} {v0} {v0} = refl
      feq n {0} {v1} {v1} = refl
      feq [] {Suc x} {()}
-     feq (_ ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) {!!} {!!}  (feq n {x} {p} {q})
+     feq (h ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) (lemma h n) (lemma h n) (feq n {x} {p} {q})
 
 record _f⊆_ (f g : PFunc) : Set (suc n) where
   field