Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1034:84881efe649b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 01 Dec 2022 18:00:44 +0900 |
| parents | 2da8dcbb0825 |
| children | 2144ef00cab9 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 64 insertions(+), 95 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Dec 01 11:31:15 2022 +0900 +++ b/src/zorn.agda Thu Dec 01 18:00:44 2022 +0900 @@ -514,7 +514,12 @@ supfa x ∎ ) a ) where open o≤-Reasoning O z53 : {z : Ordinal } → odef (UnionCF A f ay (ZChain.supf zb) x) z → odef (UnionCF A f ay (ZChain.supf za) x) z - z53 {z} ⟪ as , cp ⟫ = ⟪ as , ? ⟫ + z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ + z53 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ⟪ as , ch-is-sup u u<x (trans ua=ub su=u) z55 ⟫ where + ua=ub : supfa u ≡ supfb u + ua=ub = prev u u<x (ordtrans u<x x≤xa ) + z55 : FClosure A f (ZChain.supf za u) z + z55 = subst (λ k → FClosure A f k z ) (sym ua=ub) fc ... | tri> ¬a ¬b c = ⊥-elim ( o≤> ( begin supfa x ≡⟨ sax=spa ⟩ @@ -523,17 +528,12 @@ supfb x ∎ ) c ) where open o≤-Reasoning O z53 : {z : Ordinal } → odef (UnionCF A f ay (ZChain.supf za) x) z → odef (UnionCF A f ay (ZChain.supf zb) x) z - z53 {z} ⟪ as , cp ⟫ = ⟪ as , ? ⟫ - -UChain-eq : { A : HOD } { f : Ordinal → Ordinal } {mf : ≤-monotonic-f A f} - {z y : Ordinal} {ay : odef A y} { supf0 supf1 : Ordinal → Ordinal } - → (seq : {x : Ordinal } → x o< z → supf0 x ≡ supf1 x ) - → UnionCF A f ay supf0 z ≡ UnionCF A f ay supf1 z -UChain-eq {A} {f} {mf} {z} {y} {ay} {supf0} {supf1} seq = ==→o≡ record { eq← = ueq← ; eq→ = ueq→ } where - ueq← : {x : Ordinal} → odef A x ∧ ? → odef A x ∧ ? - ueq← {z} ⟪ ab , cp ⟫ = ⟪ ab , ? ⟫ - ueq→ : {x : Ordinal} → odef A x ∧ ? → odef A x ∧ ? - ueq→ {z} ⟪ ab , cp ⟫ = ⟪ ab , ? ⟫ + z53 ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ + z53 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ⟪ as , ch-is-sup u u<x (trans ub=ua su=u) z55 ⟫ where + ub=ua : supfb u ≡ supfa u + ub=ua = sym ( prev u u<x (ordtrans u<x x≤xa )) + z55 : FClosure A f (ZChain.supf zb u) z + z55 = subst (λ k → FClosure A f k z ) (sym ub=ua) fc Zorn-lemma : { A : HOD } → o∅ o< & A @@ -607,9 +607,9 @@ S = supP B B⊆A total s1 = & (SUP.sup S) m05 : {w : Ordinal } → odef B w → (w ≡ s1 ) ∨ (w << s1 ) - m05 {w} bw with SUP.x≤sup S ? -- ? (subst (λ k → odef B k) (sym &iso) bw ) - ... | case1 eq = case1 ( subst₂ (λ j k → j ≡ k ) &iso refl ?) -- (cong (&) eq) ) - ... | case2 lt = case2 ? -- ( subst (λ k → _ < k ) (sym *iso) lt ) + m05 {w} bw with SUP.x≤sup S bw + ... | case1 eq = case1 ( subst₂ (λ j k → j ≡ k ) &iso refl (trans &iso eq)) + ... | case2 lt = case2 lt m02 : MinSUP A B m02 = dont-or (m00 (& A)) m03 @@ -652,7 +652,10 @@ → HasPrev A (UnionCF A f ay (ZChain.supf zc) x) f b → * a < * b → odef (UnionCF A f ay (ZChain.supf zc) x) b is-max-hp x {a} {b} ua ab has-prev a<b with HasPrev.ay has-prev - ... | ⟪ ab0 , cp ⟫ = ⟪ ab , ? ⟫ + ... | ⟪ ab0 , ch-init fc ⟫ = ⟪ ab , ch-init ( subst (λ k → FClosure A f y k) (sym (HasPrev.x=fy has-prev)) (fsuc _ fc )) ⟫ + ... | ⟪ ab0 , ch-is-sup u u<x su=u fc ⟫ = ⟪ ab , subst (λ k → UChain ay x k ) + (sym (HasPrev.x=fy has-prev)) ( ch-is-sup u u<x su=u (fsuc _ fc)) ⟫ + supf = ZChain.supf zc @@ -662,7 +665,7 @@ px = Oprev.oprev op is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f ay supf x) a → b o< x → (ab : odef A b) → - HasPrev A (UnionCF A f ay supf x) f b ∨ IsSUP A (UnionCF A f ay supf b) ? → + HasPrev A (UnionCF A f ay supf x) f b ∨ IsSUP A (UnionCF A f ay supf b) b → * a < * b → odef (UnionCF A f ay supf x) b is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b @@ -674,7 +677,7 @@ m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b - m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } , m04 ⟫ + m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } , m04 ⟫ m10 : odef (UnionCF A f ay supf x) b m10 = ZChain.cfcs zc mf< b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05) ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where @@ -690,7 +693,7 @@ m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay = chain-mono1 (o<→≤ b<x) (HasPrev.ay nhp) ; x=fy = HasPrev.x=fy nhp } ) m05 : ZChain.supf zc b ≡ b - m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } , m04 ⟫ + m05 = ZChain.sup=u zc ab (o<→≤ (z09 ab) ) ⟪ record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz } , m04 ⟫ m14 : ZChain.supf zc b o< x m14 = subst (λ k → k o< x ) (sym m05) b<x m13 : odef (UnionCF A f ay supf x) z @@ -703,8 +706,8 @@ * a < * b → odef (UnionCF A f ay supf x) b is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b - is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (ZChain.chain∋init zc ? ) - ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ? ⟫ + is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (ZChain.chain∋init zc (ordtrans b<x x≤A) ) + ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl )) ⟫ ... | case2 y<b with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x)) ... | case2 sb<sx = m10 where m09 : b o< & A @@ -802,28 +805,22 @@ -- pchainpx : HOD - pchainpx = record { od = record { def = λ z → (odef A z ∧ ? ) + pchainpx = record { od = record { def = λ z → (odef A z ∧ UChain ay px z ) ∨ FClosure A f (supf0 px) z } ; odmax = & A ; <odmax = zc00 } where - zc00 : {z : Ordinal } → (odef A z ∧ ? ) ∨ FClosure A f (supf0 px) z → z o< & A + zc00 : {z : Ordinal } → (odef A z ∧ UChain ay px z ) ∨ FClosure A f (supf0 px) z → z o< & A zc00 {z} (case1 lt) = z07 lt zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf fc ) - zc02 : { a b : Ordinal } → odef A a ∧ ? → FClosure A f (supf0 px) b → a ≤ b + zc02 : { a b : Ordinal } → odef A a ∧ UChain ay px a → FClosure A f (supf0 px) b → a ≤ b zc02 {a} {b} ca fb = zc05 fb where - zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ supf0 px - zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) refl zc05 : {b : Ordinal } → FClosure A f (supf0 px) b → a ≤ b zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc (supf0 px) f mf fb )) - ... | case1 eq = subst (λ k → a ≤ k ) (subst₂ (λ j k → j ≡ k) &iso &iso ?) (zc05 fb) + ... | case1 eq = subst (λ k → a ≤ k ) eq (zc05 fb) ... | case2 lt = ≤-ftrans (zc05 fb) (case2 lt) - zc05 (init b1 refl) with MinSUP.x≤sup (ZChain.minsup zc o≤-refl) - (subst (λ k → odef A k ∧ ?) (sym &iso) ca ) - ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq ) - ... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso (cong (*) zc06) lt ) + zc05 (init b1 refl) = MinSUP.x≤sup (ZChain.minsup zc o≤-refl) ca ptotal : IsTotalOrderSet pchainpx - ptotal (case1 a) (case1 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso - ? + ptotal (case1 a) (case1 b) = ZChain.f-total zc a b ptotal {a0} {b0} (case1 a) (case2 b) with zc02 a b ... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where eq1 : a0 ≡ b0 @@ -848,17 +845,23 @@ sup1 = minsupP pchainpx pcha ptotal sp1 = MinSUP.sup sup1 - sfpx≤sp1 : supf0 px ≤ sp1 - sfpx≤sp1 = MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl )) - -- -- supf0 px o≤ sp1 -- + sfpx≤sp1 : supf0 px ≤ sp1 + sfpx≤sp1 = MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl )) + + m13 : supf0 px o≤ sp1 + m13 = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1) m14 where + m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1) + m14 {z} ⟪ as , ch-init fc ⟫ = ? + m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ? + zc41 : ZChain A f mf ay x zc41 with zc43 x sp1 zc41 | (case2 sp≤x ) = record { supf = supf1 ; sup=u = ? ; asupf = asupf1 ; supf-mono = supf1-mono ; order = ? - ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; cfcs = cfcs } where + ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where supf1 : Ordinal → Ordinal supf1 z with trio< z px @@ -937,7 +940,7 @@ -- supf0 a ≡ supf0 (supf0 a) ≡ supf0 px o< x z50 : odef (UnionCF A f ay supf1 b) w z50 with osuc-≡< px≤sa - ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , ? ⟫ where + ... | case1 px=sa = ⟪ A∋fc {A} _ f mf fc , cp ⟫ 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 @@ -955,45 +958,14 @@ supf0 (supf0 a) ≡⟨ sym (sf1=sf0 sa≤px) ⟩ supf1 (supf0 a) ≡⟨ cong supf1 (sym spx=sa) ⟩ supf1 (supf0 px) ∎ where open ≡-Reasoning - m : MinSUP A (UnionCF A f ay supf0 px) - m = ZChain.minsup zc o≤-refl - m=spx : MinSUP.sup m ≡ supf1 (supf0 px) - m=spx = begin - MinSUP.sup m ≡⟨ sym ( ZChain.supf-is-minsup zc o≤-refl) ⟩ - supf0 px ≡⟨ cong supf0 px=sa ⟩ - 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) ≡⟨ 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 : ? - cp = ? where - uz : {s z1 : Ordinal } → supf1 s o< supf1 (supf0 px) → FClosure A f (supf1 s) z1 → odef (UnionCF A f 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 = 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) ≡⟨ 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 ⟩ - supf0 a ≡⟨ sym px=sa ⟩ - px ∎ ) where open o≤-Reasoning O - order : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 (supf0 px) → - FClosure A f (supf1 s) z1 → (z1 ≡ supf1 (supf0 px)) ∨ (z1 << supf1 (supf0 px)) - order {s} {z} s<u fc = subst (λ k → (z ≡ k) ∨ ( z << k ) ) m=spx (MinSUP.x≤sup m (uz s<u fc) ) + cp : UChain ay b w + cp = ch-is-sup (supf0 px) z51 z53 (subst (λ k → FClosure A f k w) z52 fc) ... | case2 px<sa = ⊥-elim ( ¬p<x<op ⟪ px<sa , subst₂ (λ j k → j o< k ) (sf1=sf0 a≤px) (sym (Oprev.oprev=x op)) z53 ⟫ ) where z53 : supf1 a o< x z53 = ordtrans<-≤ sa<b b≤x @@ -1002,9 +974,19 @@ z50 : odef (UnionCF A f ay supf1 b) w z50 with osuc-≡< b≤x ... | case2 lt with ZChain.cfcs zc mf< a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) sa<b fc - ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ -- u o< px → u o< b ? + ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ + ... | ⟪ az , ch-is-sup u u<b su=u fc ⟫ = ⟪ az , ch-is-sup u u<b (trans (sym (sf=eq u<x)) su=u) (fcpu fc u≤px ) ⟫ where + u≤px : u o≤ px + u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ u<b b≤x ) + u<x : u o< x + u<x = ordtrans<-≤ u<b b≤x z50 | case1 eq with ZChain.cfcs zc mf< a<px o≤-refl sa<px fc - ... | ⟪ az , cp ⟫ = ⟪ az , ? ⟫ -- u o< px → u o< b ? + ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ + ... | ⟪ az , ch-is-sup u u<px su=u fc ⟫ = ⟪ az , ch-is-sup u u<b (trans (sym (sf=eq u<x)) su=u) (fcpu fc (o<→≤ u<px)) ⟫ where -- u o< px → u o< b ? + u<b : u o< b + u<b = subst (λ k → u o< k ) (trans (Oprev.oprev=x op) (sym eq) ) (ordtrans u<px <-osuc ) + u<x : u o< x + u<x = subst (λ k → u o< k ) (Oprev.oprev=x op) ( ordtrans u<px <-osuc ) ... | tri≈ ¬a a=px ¬c = csupf1 where -- a ≡ px , b ≡ x, sp o≤ x px<b : px o< b @@ -1020,7 +1002,7 @@ z53 = A∋fc {A} _ f mf fc csupf1 : odef (UnionCF A f ay supf1 b) w csupf1 with trio< (supf0 px) x - ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ? ⟫ where + ... | tri< sfpx<x ¬b ¬c = ⟪ z53 , ch-is-sup spx (subst (λ k → spx o< k) (sym b=x) sfpx<x) z52 fc1 ⟫ where spx = supf0 px spx≤px : supf0 px o≤ px spx≤px = zc-b<x _ sfpx<x @@ -1028,39 +1010,26 @@ z52 = trans (sf1=sf0 (zc-b<x _ sfpx<x)) ( ZChain.supf-idem zc mf< o≤-refl (zc-b<x _ sfpx<x ) ) fc1 : FClosure A f (supf1 spx) w fc1 = subst (λ k → FClosure A f k w ) (trans (cong supf0 a=px) (sym z52) ) fc - order : {s z1 : Ordinal} → supf1 s o< supf1 spx → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 spx) ∨ (z1 << supf1 spx) - order {s} {z1} ss<spx fcs = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) - (trans (sym (ZChain.supf-is-minsup zc spx≤px )) (sym (sf1=sf0 spx≤px) ) ) - (MinSUP.x≤sup (ZChain.minsup zc spx≤px) (ZChain.cfcs zc mf< (supf-inject0 supf1-mono ss<spx) - spx≤px ss0<spx (fcup fcs (ordtrans (supf-inject0 supf1-mono ss<spx) spx≤px ) ))) where - ss0<spx : supf0 s o< spx - ss0<spx = osucprev ( begin - osuc (supf0 s) ≡⟨ cong osuc (sym (sf1=sf0 ( begin - s <⟨ supf-inject0 supf1-mono ss<spx ⟩ - supf0 px ≤⟨ spx≤px ⟩ - px ∎ ) )) ⟩ - osuc (supf1 s) ≤⟨ osucc ss<spx ⟩ - supf1 spx ≡⟨ sf1=sf0 spx≤px ⟩ - supf0 spx ≤⟨ ZChain.supf-mono zc spx≤px ⟩ - supf0 px ∎ ) where open o≤-Reasoning O ... | tri≈ ¬a spx=x ¬c = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf0 px) (ZChain.asupf zc)))) where -- supf px ≡ x then the chain is stopped, which cannot happen when <-monotonic case m12 : supf0 px ≡ sp1 - m12 with osuc-≡< ? -- sfpx≤sp1 + m12 with osuc-≡< m13 ... | case1 eq = eq - ... | case2 lt = ⊥-elim ( o≤> sp≤x (subst (λ k → k o< sp1) spx=x lt )) -- supf0 px o< sp1 , x o< sp1 + ... | case2 lt = ⊥-elim ( o≤> sp≤x (subst (λ k → k o< sp1) spx=x lt )) m10 : f (supf0 px) ≡ supf0 px m10 = fc-stop A f mf (ZChain.asupf zc) m11 m12 where m11 : {z : Ordinal} → FClosure A f (supf0 px) z → (z ≡ sp1) ∨ (z << sp1) m11 {z} fc = MinSUP.x≤sup sup1 (case2 fc) - ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans ? sp≤x))) -- x o< supf0 px o≤ sp1 ≤ x + ... | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (ordtrans<-≤ c (OrdTrans m13 sp≤x))) -- x o< supf0 px o≤ sp1 ≤ x ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) ( ordtrans<-≤ a<b b≤x) ⟫ ) -- px o< a o< b o≤ x zc11 : {z : Ordinal} → odef (UnionCF A f ay supf1 x) z → odef pchainpx z - zc11 {z} ⟪ az , cp ⟫ = zc21 ? where - zc21 : {z1 : Ordinal } → FClosure A f (supf1 ?) z1 → odef pchainpx z1 + zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ + zc11 {z} ⟪ az , ch-is-sup u u<x su=u fc ⟫ = zc21 fc where + zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc - ... | case1 ⟪ ua1 , cp ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ? ⟫ + ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ + ... | case1 ⟪ ua1 , ch-is-sup u u<x su=u fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x su=u (fsuc _ fc₁) ⟫ ... | case2 fc = case2 (fsuc _ fc) zc21 (init asp refl ) = ?