# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1563521806 -32400
# Node ID ad7a6185b6d5ad98a56f4b484cc0954a33ad8770
# Parent  e6e1bdbda450b824c015887c1606c53886ac791e
...

diff -r e6e1bdbda450 -r ad7a6185b6d5 HOD.agda
--- a/HOD.agda	Fri Jul 19 15:28:20 2019 +0900
+++ b/HOD.agda	Fri Jul 19 16:36:46 2019 +0900
@@ -285,12 +285,14 @@
             lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly       -- z(b)
             ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c )))
             lemma z lt | case2 lz=ly | tri≈ ¬a refl ¬c with d<→lv lz=ly    -- z(c)
-            ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx
-               (ox lz=ly  -- ord (od→ord z) d< ord (od→ord (ord→od (record { lv = lx ; ord = oy })))
-                    (subst (λ k → lv (od→ord z) ≡ k ) lemma1 eq) ) {_} {ord (od→ord z)} (case2 {!!})) where
-                 ox : {lx lz : Nat} → {oy : OrdinalD {suc n} lz} {oz : OrdinalD {suc n} lx} → {!!} d< {!!} → lz ≡ lx → OrdinalD {suc n} lx
-                 ox = ?
-             
+            ... | eq = subst ( λ k → ψ k ) oiso (lemma6 {lx} {lv (od→ord (ord→od (record { lv = lx ; ord = oy })))} {lv (od→ord z)}
+                        {oy} {_} (sym lemma1) (sym eq) (trans (sym lemma1) (sym eq)) lz=ly )  where
+                  lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z
+                  lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt )
+                  lemma6 : { lx ly lz : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } { oz : OrdinalD {suc n} lz } →
+                       lx ≡ ly → ly ≡ lz → lx ≡ lz   → oz d< oy → ψ (ord→od ( record { lv = lz ; ord = oz} ))
+                  lemma6 {lx} {ly} {lz} {ox} {oy} {oz} refl refl refl _ =  ? -- subst  ( λ k → ψ k ) (sym oiso) ( lemma5 {!!} {!!} )
+
 
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record {