--- a/partfunc.agda	Sat Jul 25 09:09:00 2020 +0900
+++ b/partfunc.agda	Sat Jul 25 12:54:28 2020 +0900
@@ -209,25 +209,7 @@
       lemma2 (just i1 ∷ p) = lemma2 p
       lemma2 (nothing ∷ p) = lemma2 p
 
-record 3Gf (f : Nat → Two) (p : List (Maybe Two)) : Set where
-   field
-     3gn  : Nat
-     3f<n : p 3⊆ (f 3↑ 3gn)
-
-open 3Gf
-
-min  = Data.Nat._⊓_
+-- min  = Data.Nat._⊓_
 -- m≤m⊔n  = Data.Nat._⊔_
-open import Data.Nat.Properties
+-- open import Data.Nat.Properties
 
-3GF : {n : Level } → (Nat → Two ) → F-Filter (List (Maybe Two)) (λ x → One) _3⊆_ _3∩_
-3GF {n} f = record {  
-       filter = λ p → 3Gf f p
-     ; f⊆P = OneObj
-     ; filter1 = λ {p} {q} _ fp p⊆q → lemma1 p q fp p⊆q
-     ; filter2 = λ {p} {q} fp fq  → record { 3gn = min (3gn fp) (3gn fq) ; 3f<n = lemma2 p q fp fq }
- }  where
-      lemma1 : (p q : List (Maybe Two) ) → (fp : 3Gf f p) →  (p⊆q : p 3⊆ q) → 3Gf f q
-      lemma1 p q fp p⊆q  = record { 3gn = 3gn fp  ; 3f<n = {!!} }
-      lemma2 : (p q : List (Maybe Two) ) → (fp : 3Gf f p) → (fq : 3Gf f q)  → (p 3∩ q) 3⊆ (f 3↑ min (3gn fp) (3gn fq))
-      lemma2 p q fp fq = ?