# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669416669 -32400
# Node ID 8b3d7c461a84c7bf0913f1d2e2ea417be4cd714c
# Parent  e4919cc0cfe898fe08c851ae9cbf0fbf7d3bb1d8
...

diff -r e4919cc0cfe8 -r 8b3d7c461a84 src/zorn.agda
--- a/src/zorn.agda	Fri Nov 25 23:39:04 2022 +0900
+++ b/src/zorn.agda	Sat Nov 26 07:51:09 2022 +0900
@@ -1070,17 +1070,20 @@
                       ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ch-is-sup (supf0 px) z51 cp (subst (λ k → FClosure A f k w) z52 fc)  ⟫ where
                           sa≤px : supf0 a o≤ px
                           sa≤px = subst₂ (λ j k → j o< k) px=sa (sym (Oprev.oprev=x op)) px<x
+                          spx=sa : supf0 px ≡ supf0 a
+                          spx=sa = begin
+                                supf0 px ≡⟨ cong supf0 px=sa  ⟩ 
+                                supf0 (supf0 a) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px  ⟩
+                                supf0 a ∎  where open ≡-Reasoning
                           z51 : supf0 px o< b
-                          z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ cong supf0 px=sa ⟩ 
-                                supf0 (supf0 a ) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px ⟩ 
+                          z51 = subst (λ k → k o< b ) (sym ( begin supf0 px ≡⟨ spx=sa ⟩ 
                                 supf0 a ≡⟨ sym (sf1=sf0 a≤px) ⟩ 
                                 supf1 a ∎ )) sa<b where open ≡-Reasoning
                           z52 : supf1 a ≡ supf1 (supf0 px)
                           z52 = begin supf1 a ≡⟨ sf1=sf0 a≤px ⟩ 
                                 supf0 a ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩ 
                                 supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px)  ⟩ 
-                                supf1 (supf0 a) ≡⟨ cong supf1 (sym (ZChain.supf-idem zc mf< a≤px sa≤px )) ⟩ 
-                                supf1 (supf0 (supf0 a)) ≡⟨ cong (λ k → supf1 (supf0 k)) (sym px=sa)  ⟩ 
+                                supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩ 
                                 supf1 (supf0 px) ∎ where open ≡-Reasoning
                           m : MinSUP A (UnionCF A f mf ay supf0 px)
                           m = ZChain.minsup zc o≤-refl
@@ -1088,15 +1091,13 @@
                           m=spx = begin 
                                 MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc o≤-refl)  ⟩ 
                                 supf0 px ≡⟨ cong supf0 px=sa  ⟩ 
-                                supf0 (supf0 a) ≡⟨ ZChain.supf-idem zc mf< a≤px sa≤px  ⟩
-                                supf0 a ≡⟨ sym (sf1=sf0 a≤px)  ⟩ 
-                                supf1 a ≡⟨ z52  ⟩ 
+                                supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px)  ⟩
+                                supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa)  ⟩
                                 supf1 (supf0 px)  ∎  where open ≡-Reasoning 
                           z53 : supf1 (supf0 px) ≡ supf0 px
                           z53 = begin
-                                supf1 (supf0 px)  ≡⟨ sym z52 ⟩ 
-                                supf1 a  ≡⟨ sf1=sf0 a≤px ⟩ 
-                                supf0 a  ≡⟨ sym (ZChain.supf-idem zc mf< a≤px sa≤px ) ⟩ 
+                                supf1 (supf0 px)  ≡⟨ cong supf1 spx=sa ⟩ 
+                                supf1 (supf0 a)  ≡⟨ sf1=sf0 sa≤px ⟩ 
                                 supf0 (supf0 a)  ≡⟨ sym ( cong supf0 px=sa ) ⟩ 
                                 supf0 px  ∎  where open ≡-Reasoning 
                           cp : ChainP A f mf ay supf1 (supf0 px)
@@ -1106,15 +1107,17 @@
                              uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f mf ay supf0 px) z1
                              uz {s} {z1} ss<sp fc = ZChain.cfcs zc mf< s<px o≤-refl ss<px (subst (λ k → FClosure A f k z1) 
                                      (sf1=sf0 (o<→≤ s<px))  fc ) where
+                                s<spx : s o< supf0 px
+                                s<spx = supf-inject0 supf1-mono ss<sp
                                 s<px : s o< px
-                                s<px = ZChain.supf-inject zc (osucprev ( begin
-                                     osuc (supf0 s)  ≡⟨ sym (cong osuc (sf1=sf0 ?) )  ⟩  
-                                     osuc (supf1 s)  ≤⟨ osucc ss<sp  ⟩ 
-                                     supf1 (supf0 px)  ≡⟨ z53  ⟩ 
-                                     supf0 px ∎ ))   where open o≤-Reasoning O
+                                s<px = osucprev ( begin
+                                     osuc s  ≤⟨  osucc s<spx   ⟩  
+                                     supf0 px  ≡⟨ spx=sa  ⟩ 
+                                     supf0 a ≡⟨ sym px=sa  ⟩ 
+                                     px ∎ )   where open o≤-Reasoning O
                                 ss<px : supf0 s o< px
                                 ss<px = osucprev ( begin
-                                     osuc (supf0 s)  ≡⟨ sym (cong osuc (sf1=sf0 ?) )  ⟩ 
+                                     osuc (supf0 s)  ≡⟨ cong osuc (sym (sf1=sf0 (o<→≤ s<px)))  ⟩ 
                                      osuc (supf1 s)  ≤⟨ osucc ss<sp  ⟩ 
                                      supf1 (supf0 px)  ≡⟨ sym z52  ⟩ 
                                      supf1 a  ≡⟨ sf1=sf0 a≤px  ⟩