# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1666595775 -32400
# Node ID f160556a7c9af45f337021fe45844ced27c7437e
# Parent  ed711d7be1913c97cbd441b2efba57b926432217
...

diff -r ed711d7be191 -r f160556a7c9a src/zorn.agda
--- a/src/zorn.agda	Mon Oct 24 16:06:18 2022 +0900
+++ b/src/zorn.agda	Mon Oct 24 16:16:15 2022 +0900
@@ -1366,9 +1366,7 @@
            z22 : sp o< & A
            z22 = z09 asp
            x<sup : {x : HOD} → chain ∋ x → (x ≡ SUP.sup sp1 ) ∨ (x < SUP.sup sp1 )
-           x<sup bz with SUP.x<sup sp1 bz 
-           ... | case1 eq = case1 ?
-           ... | case2 lt = case2 ?
+           x<sup bz = SUP.x<sup sp1 bz 
            z12 : odef chain sp
            z12 with o≡? (& s) sp
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
@@ -1397,12 +1395,12 @@
                ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
            ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
            ... | tri> ¬a ¬b c = ⊥-elim z17 where
-               z15 : (* (f sp) ≡ SUP.sup sp1) ∨ (* (f sp) <  * sp )
-               z15  = ? -- x<sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
+               z15 : (* (f sp) ≡ SUP.sup sp1) ∨ (* (f sp) <  SUP.sup sp1 )
+               z15  = x<sup (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
                z17 : ⊥
                z17 with z15
                ... | case1 eq = ¬b eq
-               ... | case2 lt = ¬a ?
+               ... | case2 lt = ¬a lt
 
 
      -- ZChain contradicts ¬ Maximal