--- a/OD.agda	Fri Aug 02 12:17:10 2019 +0900
+++ b/OD.agda	Fri Aug 02 16:27:53 2019 +0900
@@ -308,6 +308,31 @@
     ｛_｝ : ZFSet → ZFSet
     ｛ x ｝ = ( x ,  x )
 
+    u-osuc : { x : Ordinal {suc n}} → Union (ord→od x , (ord→od x , ord→od x )) == ord→od (osuc x)
+    u-osuc {x} = record { eq→ = lemma1 ; eq← = lemma2 } where
+        lemma1 : {y : Ordinal} → def (Union (ord→od x , (ord→od x , ord→od x))) y → def (ord→od (osuc x)) y
+        lemma1 {y} lt = {!!}
+        lemma2 : {y : Ordinal} → def (ord→od (osuc x)) y → def (Union (ord→od x , (ord→od x , ord→od x))) y
+        lemma2 {y} lt not = {!!}
+
+    union-ord : { x : Ordinal {suc n}} → Union (Ord x) == record { def = λ y → osuc y o< x }
+    union-ord {x} = record { eq→ = lemma1 ; eq← = lemma2 } where
+         lemma1 : {y : Ordinal} → def (Union (Ord x)) y → osuc y o< x
+         lemma1 {y} lt with trio< (osuc y) x
+         lemma1 {y} lt | tri< a ¬b ¬c = a
+         lemma1 {y} lt | tri≈ ¬a refl ¬c = ⊥-elim ( lt (λ u → lemma3 {u}) ) where
+             lemma3 : {u : Ordinal} → (u o< osuc y) ∧ def (ord→od u) y → ⊥
+             lemma3 {u} lt with osuc-≡< (proj1 lt)
+             lemma3 {u} lt | case1 refl = o<¬≡ refl (o<-subst ( def→o< {n} {ord→od u} (proj2 lt)) (sym diso) refl )
+             lemma3 {u} lt | case2 lt1 = o<> lt1 (o<-subst ( def→o< {n} {ord→od u} (proj2 lt)) refl diso )
+         lemma1 {y} lt | tri> ¬a ¬b c = ⊥-elim ( lt (λ u → lemma4 {u} ) ) where
+             lemma4 : {u : Ordinal} → (u o< x) ∧ def (ord→od u) y → ⊥  -- c : x o< osuc y
+             lemma4 {u} lt with osuc-≡< c
+             lemma4 {u} lt | case1 refl = o<> (proj1 lt) (o<-subst ( def→o< {n} {ord→od u} (proj2 lt)) refl diso )
+             lemma4 {u} lt | case2 lt1 = o<> ( ordtrans ( proj1 lt)  lt1 ) (o<-subst ( def→o< {n} {ord→od u} (proj2 lt)) refl diso )
+         lemma2 : {y : Ordinal} → osuc y o< x → def (Union (Ord x)) y
+         lemma2 {y} lt not = not (osuc y) record { proj1 = lt ; proj2 = {!!} } -- lt :  def (Ord x) (osuc y)
+
     data infinite-d  : ( x : Ordinal {suc n} ) → Set (suc n) where
         iφ :  infinite-d o∅
         isuc : {x : Ordinal {suc n} } →   infinite-d  x  →