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

diff src/PFOD.agda @ 1096:55ab5de1ae02

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
recovery
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2022 12:54:05 +0900
parents e787d37d27a0
children c2501d308c95
line wrap: on
line diff
--- a/src/PFOD.agda	Thu Dec 22 15:10:31 2022 +0900
+++ b/src/PFOD.agda	Fri Dec 23 12:54:05 2022 +0900
@@ -130,8 +130,6 @@
 ω→2f≡i1 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω))
 ω→2f≡i1 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p
 
-open _⊆_
-
 -- someday ...
 -- postulate 
 --    ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt )  =h= X