--- a/src/OD.agda	Thu Dec 22 15:10:31 2022 +0900
+++ b/src/OD.agda	Fri Dec 23 12:54:05 2022 +0900
@@ -265,11 +265,9 @@
 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }
         ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))}
 
-record _⊆_ ( A B : HOD   ) : Set (suc n) where
-  field
-     incl : { x : HOD } → A ∋ x →  B ∋ x
+_⊆_ : ( A B : HOD)   → Set n
+_⊆_ A B = { x : Ordinal } → odef A x → odef B x
 
-open _⊆_
 infixr  220 _⊆_
 
 -- if we have & (x , x) ≡ osuc (& x),  ⊆→o≤ → c<→o<
@@ -298,28 +296,6 @@
      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy)
      ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (* oy)} induction oy
 
-record OSUP (A x : Ordinal ) ( ψ : ( x : Ordinal ) → odef (* A) x →  Ordinal ) : Set n where
-   field
-      sup-o'  :   Ordinal
-      sup-o≤' :  {z : Ordinal } → z o< x → (lt : odef (* A) z ) → ψ z lt o≤  sup-o' 
-
--- o<-sup :  ( A x : Ordinal) { ψ : ( x : Ordinal ) → odef (* A) x →  Ordinal } → OSUP A x ψ
--- o<-sup A x {ψ} = ? where
---   m00 : (x : Ordinal ) → OSUP A x ψ
---   m00 x = Ordinals.inOrdinal.TransFinite0 O ind x where
---      ind : (x : Ordinal) → ((z : Ordinal) → z o< x → OSUP A z ψ ) → OSUP A x ψ
---      ind x prev  =  ? where
---        if has prev , od01 is empty use prev (cannot be odef (* A) x)
---                              not empty, take larger
---           limit ordinal, take address of Union
---
---          od01 : HOD
---          od01 = record { od = record { def = λ z → odef A z ∧ ( z ≡ & x ) } ; odmax = & A ; <odmax = odef∧<  }
---          m01 : OSUP A x ψ 
---          m01 with is-o∅ (& od01 )
---          ... | case1 t=0 = record { sup-o' = prevjjk
---          ... | case2 t>0 = ?
-
 -- Open supreme upper bound leads a contradition, so we use domain restriction on sup
 ¬open-sup : ( sup-o : (Ordinal →  Ordinal ) → Ordinal) → ((ψ : Ordinal →  Ordinal ) → (x : Ordinal) → ψ x  o<  sup-o ψ ) → ⊥
 ¬open-sup sup-o sup-o< = o<> <-osuc (sup-o< next-ord (sup-o next-ord)) where
@@ -468,13 +444,13 @@
 pair← x y t (case2 t=h=y) = case2 (cong (λ k → & k ) (==→o≡ t=h=y))
 
 o<→c< :  {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y)
-o<→c< lt = record { incl = λ z → ordtrans z lt }
+o<→c< lt {z} ox = ordtrans ox lt
 
 ⊆→o< :  {x y : Ordinal } → (Ord x) ⊆ (Ord y) →  x o< osuc y
 ⊆→o< {x} {y}  lt with trio< x y
 ⊆→o< {x} {y}  lt | tri< a ¬b ¬c = ordtrans a <-osuc
 ⊆→o< {x} {y}  lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
-⊆→o< {x} {y}  lt | tri> ¬a ¬b c with (incl lt)  (o<-subst c (sym &iso) refl )
+⊆→o< {x} {y}  lt | tri> ¬a ¬b c with lt  (o<-subst c (sym &iso) refl )
 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt &iso refl ))
 
 ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y