--- a/filter.agda	Tue Jul 21 21:32:58 2020 +0900
+++ b/filter.agda	Tue Jul 21 23:40:38 2020 +0900
@@ -359,6 +359,11 @@
 _3↑_ : (Nat → Two) → Nat → List Three
 f 3↑ x = ↑app f x [] 
 
+lemma10 : (s t : List Three ) → (s 3⊆ t) → ((j0 ∷ s) 3⊆ (j0 ∷ t))
+lemma10 s t eq = eq 
+lemma11 : (s t : List Three ) → (s 3⊆ t) → ((j1 ∷ s) 3⊆ (j1 ∷ t))
+lemma11 s t eq = eq
+
 3↑22 : (f : Nat → Two) (i j : Nat) → List Three
 3↑22 f Zero j = []
 3↑22 f (Suc i) j with f i
@@ -368,10 +373,20 @@
 3↑2 : (Nat → Two) → Nat → List Three
 3↑2 f i = 3↑22 f i 0 
 
-lemma10 : (s t : List Three ) → (s 3⊆ t) → ((j0 ∷ s) 3⊆ (j0 ∷ t))
-lemma10 s t eq = eq 
-lemma11 : (s t : List Three ) → (s 3⊆ t) → ((j1 ∷ s) 3⊆ (j1 ∷ t))
-lemma11 s t eq = eq
+3↑<22 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑2 f x)  3⊆ (3↑2 f y)
+3↑<22 {f} {x} {y} x<y = lemma x y 0 x<y where
+     lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i )
+     lemma 0 y i z≤n with f i
+     lemma Zero Zero i z≤n | i0 = refl
+     lemma Zero (Suc y) i z≤n | i0 = 3⊆-[]  {3↑22 f (Suc y) i}
+     lemma Zero Zero i z≤n | i1 = refl
+     lemma Zero (Suc y) i z≤n | i1 = 3⊆-[]  {3↑22 f (Suc y) i}
+     lemma (Suc x) (Suc y) i (s≤s x<y) with f i  | 3↑22 f (Suc y) i
+     lemma (Suc x) (Suc y) i (s≤s x<y) | i0 | t = {!!}  where
+     lemma (Suc x) (Suc y) i (s≤s x<y) | i1 | t = {!!}
+     lemma1 : {x i : Nat} → f x ≡ i0 → 3↑22 f (Suc x) i ≡ j0 ∷ 3↑22 f x (Suc i)
+     lemma1 {x} {i} eq = {!!}
+
 lemma12 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j0 ∷ t))
 lemma12 s t eq = eq
 lemma13 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j1 ∷ t))
@@ -379,41 +394,8 @@
 lemma14 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j2 ∷ t))
 lemma14 s t eq = eq
 
-3↑<2 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑2 f x)  3⊆ (3↑2 f y)
-3↑<2 {f} {x} {y} x<y  = lemma x 0 y x<y (3↑22 f x 0)  (3↑22 f y 0) where
-    lemma :  (i j y : Nat) → i ≤ y → (s t : List Three) → s  3⊆  t
-    lemma Zero j y z≤n [] [] = refl
-    lemma Zero j y z≤n [] (x ∷ t) = 3⊆-[] {x ∷ t}
-    lemma Zero j y z≤n (x ∷ s) [] = {!!}
-    lemma Zero j y z≤n (j0 ∷ s) (j0 ∷ t) = lemma Zero j y z≤n s t
-    lemma Zero j y z≤n (j0 ∷ s) (j1 ∷ t) = {!!}
-    lemma Zero j y z≤n (j0 ∷ s) (j2 ∷ t) = {!!}
-    lemma Zero j y z≤n (j1 ∷ s) (j0 ∷ t) = {!!}
-    lemma Zero j y z≤n (j1 ∷ s) (j1 ∷ t) = lemma Zero j y z≤n s t
-    lemma Zero j y z≤n (j1 ∷ s) (j2 ∷ t) = {!!}
-    lemma Zero j y z≤n (j2 ∷ s) (j0 ∷ t) = lemma Zero j y z≤n s t
-    lemma Zero j y z≤n (j2 ∷ s) (j1 ∷ t) = lemma Zero j y z≤n s t
-    lemma Zero j y z≤n (j2 ∷ s) (j2 ∷ t) = lemma Zero j y z≤n s t
-    lemma (Suc i) j (Suc y) (s≤s i<y) [] t = 3⊆-[] {t}
-    lemma (Suc i) j (Suc y) (s≤s i<y) (x ∷ s) [] = {!!}
-    lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j0 ∷ t) = {!!}
-    lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j1 ∷ t) = {!!}
-    lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j2 ∷ t) = {!!}
-    lemma (Suc i) j (Suc y) (s≤s i<y) (j1 ∷ s) (x1 ∷ t) = {!!}
-    lemma (Suc i) j (Suc y) (s≤s i<y) (j2 ∷ s) (x1 ∷ t) = {!!}
-    -- with lemma i j y i<y s t 
-
-
 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (f 3↑ x)  3⊆ (f 3↑ y)
-3↑< {f} {x} {y} x<y = {!!} where
-    lemma0 : (i : Nat) → (y : List Three ) → ( ↑app f (Suc i) y ≡ ↑app f i (j0 ∷ y)) ∨ ( ↑app f (Suc i) y ≡ ↑app f i (j1 ∷ y))
-    lemma0 i y with f i
-    lemma0 i y | i0 = case1 refl
-    lemma0 i y | i1 = case2 refl
-    lemma : (i : Nat) → (f 3↑ i)  3⊆ (f 3↑ Suc i)
-    lemma i with f i
-    lemma i | i0 = {!!}
-    lemma i | i1 = {!!}
+3↑< {f} {x} {y} x<y = {!!} 
 
 record Finite3 (p : List Three ) : Set  where
    field