# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1563788205 -32400
# Node ID a002ce0346dd2aeb0e26768d93b1380005c4b0db
# Parent  65e1b2e415bb8e4287ce452e8d59addb3fc3abf8
...

diff -r 65e1b2e415bb -r a002ce0346dd OD.agda
--- a/OD.agda	Mon Jul 22 17:31:52 2019 +0900
+++ b/OD.agda	Mon Jul 22 18:36:45 2019 +0900
@@ -525,22 +525,3 @@
                                lx ≡ ly → ly ≡ lv (od→ord z)  → ψ z 
                           lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl)
 
-         ==→o≡' : {n : Level} →  { x y : OD {suc n} } → (x == y) → x ≡ y
-         ==→o≡' {n} {x} {y} eq = lemma1 {!!}  where
-            lemma4 : { x y : OD {suc n} } → (x == y) →  ¬ ( od→ord x o< od→ord y  )
-            lemma4 = {!!}
-            lemma3 : { x y : OD {suc n} } → (x == y) →  od→ord x ≡ od→ord y 
-            --       x  <   y
-            --    m     m 
-            lemma3 {x} {y} eq with trio< (od→ord x) (od→ord y)
-            lemma3 {x} {y} eq | tri≈ ¬a b ¬c = b
-            lemma3 {x} {y} eq | tri< a ¬b ¬c = {!!}
-            lemma3 {x} {y} eq | tri> ¬a ¬b c = {!!} 
-            lemma1 : { x y : OD {suc n} } → Ord (od→ord x) == Ord (od→ord y)  → x ≡ y
-            lemma1 {x} {y} eq = subst₂ (λ k j → k ≡ j ) oiso oiso (cong (λ k → ord→od k ) lemma2) where
-                 lemma2 : (od→ord x) ≡ (od→ord y)
-                 lemma2 with trio< (od→ord x) (od→ord y)
-                 lemma2 | tri≈ ¬a b ¬c = b
-                 lemma2 | tri< a ¬b ¬c with eq← eq a
-                 ... | lt = ⊥-elim ( o<¬≡ refl lt )
-                 lemma2 | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl ( eq→ eq c ))