# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559526603 -32400
# Node ID c07c548b2ac1030820f879332bec295364e8d4d3
# Parent  9a7a64b2388c696fa377c17395b1e4b3c7c77fa6
add some lemma

diff -r 9a7a64b2388c -r c07c548b2ac1 ordinal-definable.agda
--- a/ordinal-definable.agda	Mon Jun 03 10:19:52 2019 +0900
+++ b/ordinal-definable.agda	Mon Jun 03 10:50:03 2019 +0900
@@ -183,6 +183,12 @@
 ... | oyx with o<¬≡ (od→ord x) (od→ord x) refl (c<→o< oyx )
 ... | ()
 
+==→o≡ : {n : Level} →  { x y : Ordinal {suc n} } → ord→od x == ord→od y →  x ≡ y 
+==→o≡ {n} {x} {y} eq with trio< {n} x y
+==→o≡ {n} {x} {y} eq | tri< a ¬b ¬c = ⊥-elim ( o<→o> eq (o<-subst a (sym ord-iso) (sym ord-iso )))
+==→o≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b
+==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso )))
+
 o<→¬== : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (x == y )
 o<→¬== {n} {x} {y} lt eq = o<→o> eq lt
 
@@ -237,7 +243,7 @@
      lemma o∅ ne | yes refl | ()
      lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅→od∅ (o<→c< (∅5 ¬p))  
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record {