--- a/ordinal-definable.agda	Sat Jun 01 18:17:24 2019 +0900
+++ b/ordinal-definable.agda	Sat Jun 01 19:19:40 2019 +0900
@@ -360,7 +360,8 @@
              lemma {oz} {ooz} lt = def-subst {suc n} {ord→od  ooz} (o<→c< lt) refl diso
          union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
          union→ X y u xx with trio< ( od→ord u ) ( osuc ( od→ord y ))
-         union→ X y u xx | tri< a ¬b ¬c = {!!}
+         union→ X y u xx | tri< a ¬b ¬c with  osuc-< a (c<→o< (proj2 xx))
+         union→ X y u xx | tri< a ¬b ¬c | ()
          union→ X y u xx | tri≈ ¬a b ¬c = lemma b (c<→o< (proj1 xx )) where
              lemma : {oX ou ooy : Ordinal {suc n}} →  ou ≡ ooy  → ou o< oX   → ooy  o< oX
              lemma refl lt = lt