Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff BAlgbra.agda @ 276:6f10c47e4e7a
separate choice
fix sup-o
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 09 May 2020 09:02:52 +0900 |
| parents | 985a1af11bce |
| children | d9d3654baee1 |
line wrap: on
line diff
--- a/BAlgbra.agda Sat Apr 25 15:09:17 2020 +0900 +++ b/BAlgbra.agda Sat May 09 09:02:52 2020 +0900 @@ -5,6 +5,7 @@ open import zf open import logic import OD +import ODC open import Relation.Nullary open import Relation.Binary @@ -40,7 +41,7 @@ lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) ) lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) ) lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x - lemma3 not = double-neg-eilm (FExists _ lemma4 not) -- choice + lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not) -- choice lemma2 : {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x}))