--- a/src/partfunc.agda	Sat Feb 18 11:51:22 2023 +0900
+++ b/src/partfunc.agda	Tue Feb 21 12:02:41 2023 +0900
@@ -8,6 +8,7 @@
 open import logic
 open import Relation.Binary 
 open import Data.Empty 
+open import Data.Unit using ( ⊤ ; tt )
 open import Data.List hiding (filter)
 open import Data.Maybe  
 open import Relation.Binary
@@ -218,10 +219,10 @@
        dense-p :  { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p) 
 
 
-Dense-3 : F-Dense (List (Maybe Two) ) (λ x → One) _3⊆_ _3∩_
+Dense-3 : F-Dense (List (Maybe Two) ) (λ x → ⊤ ) _3⊆_ _3∩_
 Dense-3 = record {
        dense =  λ x → Finite3b x ≡ true
-    ;  d⊆P = OneObj
+    ;  d⊆P = tt
     ;  dense-f = λ x → finite3cov x
     ;  dense-d = λ {p} d → lemma1 p
     ;  dense-p = λ {p} d → lemma2 p