# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558938963 -32400
# Node ID a9007b02eaa12663a5a7e6e4501cc886034dd191
# Parent  83b13f1f4f42273e1f7e8d49ff7585c331755037
tri-c<

diff -r 83b13f1f4f42 -r a9007b02eaa1 ordinal-definable.agda
--- a/ordinal-definable.agda	Mon May 27 15:00:45 2019 +0900
+++ b/ordinal-definable.agda	Mon May 27 15:36:03 2019 +0900
@@ -190,9 +190,18 @@
 o<¬≡ ox ox refl (case1 lt) =  =→¬< lt
 o<¬≡ ox ox refl (case2 (s< lt)) = trio<≡ refl lt
 
+o<→o> : {n : Level} →  { x y : OD {n} } →  (x == y ) → (od→ord x ) o< ( od→ord y) → ⊥
+o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case1 lt) with
+     yx (def-subst {n} {ord→od (od→ord y)} {od→ord (ord→od (od→ord x))} (o<→c< (case1 lt )) oiso diso )
+... | oyx with o<¬≡ (od→ord x) (od→ord x) refl (c<→o< oyx )
+... | ()
+o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case2 lt) with
+     yx (def-subst {n} {ord→od (od→ord y)} {od→ord (ord→od (od→ord x))} (o<→c< (case2 lt )) oiso diso )
+... | oyx with o<¬≡ (od→ord x) (od→ord x) refl (c<→o< oyx )
+... | ()
+
 o<→¬== : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (x == y )
-o<→¬== {n} {x} {y} (case1 lt) eq = {!!}
-o<→¬== {n} {x} {y} (case2 lt) eq = {!!}
+o<→¬== {n} {x} {y} lt eq = o<→o> eq lt
 
 o<→¬c> : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (y c< x )
 o<→¬c> {n} {x} {y} olt clt = o<> (od→ord x) (od→ord y) olt (c<→o< clt ) where