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

diff ODC.agda @ 396:8c092c042093

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 Mon, 27 Jul 2020 15:11:54 +0900
parents 8b0715e28b33
children 44a484f17f26
line wrap: on
line diff
--- a/ODC.agda	Mon Jul 27 09:29:41 2020 +0900
+++ b/ODC.agda	Mon Jul 27 15:11:54 2020 +0900
@@ -84,7 +84,7 @@
 power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
 power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (t1 t∋x) } where
    t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
-   t1 = zf.IsZF.power→ isZF A t PA∋t
+   t1 = power→ A t PA∋t
 
 OrdP : ( x : Ordinal  ) ( y : HOD  ) → Dec ( Ord x ∋ y )
 OrdP  x y with trio< x (od→ord y)