--- a/src/generic-filter.agda	Sun Mar 19 12:21:10 2023 +0900
+++ b/src/generic-filter.agda	Sun Mar 19 18:30:40 2023 +0900
@@ -351,22 +351,22 @@
 --   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
 --
 
-record valR (x : HOD) {P L : HOD} {LP : L ⊆ Power P} (C : CountableModel ) (G : GenericFilter {L} {P} LP (ctl-M C) ) : Set (Level.suc n) where
-   field
-     valx : HOD
+val< : {x y p : Ordinal} → odef (* x) ( & < * y , * p >  ) → y o< x
+val< = ?
 
-record valS (ox oy oG : Ordinal) : Set n where
+record valS (G : HOD) (x z : Ordinal) (val : (y : Ordinal) → y o< x → HOD): Set n where
    field
-     op : Ordinal
-     p∈G : odef (* oG) op
-     is-val : odef (* ox) ( & < * oy , * op >  )
+     y p : Ordinal
+     G∋p : odef G p
+     is-val : odef (* x) ( & < * y , * p >  )
+     x=valy : z ≡ & (val y (val< is-val))
 
 val : (x : HOD) {P L M : HOD } {LP : L ⊆ Power P}
     →  (G : GenericFilter {L} {P} LP M )
     →  HOD
 val x G = TransFinite {λ x → HOD } ind (& x) where
   ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD
-  ind x valy = record { od = record { def = λ y → valS x y (& (⊆-Ideal.ideal (genf G))) } ; odmax = {!!} ; <odmax = {!!} }
+  ind x valy = record { od = record { def = λ z → valS (⊆-Ideal.ideal (genf G)) x z  valy  } ; odmax = {!!} ; <odmax = {!!} }