# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564368598 -32400
# Node ID 0cefb1e4d2ccaf695345b474adf44510be7861a1
# Parent  2a5844398f1cf1350bc7353fb01c51c741ac9d30
...

diff -r 2a5844398f1c -r 0cefb1e4d2cc OD.agda
--- a/OD.agda	Mon Jul 29 11:27:33 2019 +0900
+++ b/OD.agda	Mon Jul 29 11:49:58 2019 +0900
@@ -565,12 +565,9 @@
                 → (ly < lx) ∨ (oy d< ox  ) → OD {suc n}
             lemma-ord Zero (Φ 0) (case1 ())
             lemma-ord Zero (Φ 0) (case2 ())
-            lemma-ord Zero (OSuc 0 ox) lt with ∋-p X (ord→od record { lv = Zero ; ord = OSuc 0 ox })
-            lemma-ord Zero (OSuc Zero ox) lt | yes p = ord→od record { lv = Zero ; ord = OSuc 0 ox }
-            lemma-ord Zero (OSuc Zero ox) {ly} {oy} lt | no ¬p = lemma-ord Zero ox {!!}
-            lemma-ord (Suc lx) (OSuc (Suc lx) ox) lt with ∋-p X (ord→od record { lv = (Suc lx)  ; ord = ox } )
-            lemma-ord (Suc lx) (OSuc (Suc lx) ox) lt | yes p = ord→od record { lv = (Suc lx)  ; ord = ox } 
-            lemma-ord (Suc lx) (OSuc (Suc lx) ox) {ly} {oy} lt | no ¬p = lemma-ord (Suc lx) ox {!!}
+            lemma-ord lx (OSuc lx ox) lt with ∋-p X (ord→od record { lv = lx ; ord = OSuc lx ox })
+            lemma-ord lx (OSuc lx ox) lt | yes p = ord→od record { lv = lx ; ord = OSuc lx ox }
+            lemma-ord lx (OSuc lx ox) {ly} {oy} lt | no ¬p = lemma-ord lx ox {ly} {oy} {!!}
             lemma-ord (Suc lx) (Φ (Suc lx)) lt with ∋-p X (ord→od record { lv = Suc lx ; ord = Φ (Suc lx)})
             lemma-ord (Suc lx) (Φ (Suc lx)) lt | yes p = ord→od record { lv = Suc lx ; ord = Φ (Suc lx)}
-            lemma-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} lt | no ¬p = {!!}
+            lemma-ord (Suc lx) (Φ .(Suc lx)) {ly} {oy} (case1 lt ) | no ¬p = {!!}