Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1049:e6b9de04d0ca

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 07 Dec 2022 21:02:52 +0900
parents a8d6ac036d88
children 323e6e6622a2
files src/zorn.agda
diffstat 1 files changed, 3 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Wed Dec 07 20:56:57 2022 +0900
+++ b/src/zorn.agda	Wed Dec 07 21:02:52 2022 +0900
@@ -1154,12 +1154,13 @@
                      zc36 : sp1 ≡ x   -- this cannot heppen because 
                      zc36 with osuc-≡< zc31
                      ... | case1 eq = trans eq (sym x=b)
-                     ... | case2 sp1<b = ⊥-elim ? where
+                     ... | case2 sp1<b = ⊥-elim (¬p<x<op ⟪ ? , ? ⟫ ) where
                         --   sp1 o< x → ⊥
                         --   supf0 px o≤ sp1 o< x → supf0 px o≤ px
                         --        px o≤ supf0 px → px ≡ spuf0 px o≤ spuf1 x o< x
+                        --        px ≡ supf1 x
                         sp1<x : sp1 o<  x
-                        sp1<x = subst (λ k → sp1 o< k ) ? sp1<b
+                        sp1<x = subst (λ k → sp1 o< k ) (sym x=b) sp1<b
                         zc38 : supf0 px o≤ px
                         zc38 = begin
                            supf0 px  ≡⟨ sym (sf1=sf0 o≤-refl)  ⟩