# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564615700 -32400
# Node ID 64ef1db53c499e8d4644914b9a83e8521ef25eb1
# Parent  3e4eb4da14532dcbea18d357d22c0bb28ed7532d
...

diff -r 3e4eb4da1453 -r 64ef1db53c49 OD.agda
--- a/OD.agda	Thu Aug 01 00:13:07 2019 +0900
+++ b/OD.agda	Thu Aug 01 08:28:20 2019 +0900
@@ -567,18 +567,18 @@
          choice-func' X ∋-p not = have_to_find 
            where
             ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n))
-            ψ ox = ( x : Ordinal {suc n}) → x o< ox  → ¬ (def X x ) ∨ choiced X
+            ψ ox = ( x : Ordinal {suc n}) → x o< ox  → ( ¬ def X x ) ∨ choiced X
             lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox
             lemma-ord  ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc ox where
                caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) ) 
                caseΦ lx prev with ∋-p X ( ord→od (ordinal lx (Φ lx) ))
-               caseΦ lx prev | yes p = ? -- case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
-               caseΦ lx prev | no ¬p = ?
+               caseΦ lx prev | yes p = {!!} -- case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
+               caseΦ lx prev | no ¬p = {!!}
                caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) )
                caseOSuc lx x prev with ∋-p X (ord→od record { lv = lx ; ord = x } )
-               caseOSuc lx x prev | yes p = ? -- case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
-               caseOSuc lx x prev | no ¬p =  ?
+               caseOSuc lx x prev | yes p = {!!} -- case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
+               caseOSuc lx x prev | no ¬p =  {!!}
             have_to_find : choiced X
             have_to_find with lemma-ord (od→ord X )
-            have_to_find | t = ?
+            have_to_find | t = dont-or ( t (od→ord X) {!!} ) {!!}
 
diff -r 3e4eb4da1453 -r 64ef1db53c49 zf.agda
--- a/zf.agda	Thu Aug 01 00:13:07 2019 +0900
+++ b/zf.agda	Thu Aug 01 08:28:20 2019 +0900
@@ -37,6 +37,10 @@
 de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
 de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
 
+dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
+dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
+dont-or {A} {B} (case2 b) ¬A = b
+
 -- mid-ex-neg : {n  : Level } {A : Set n} → ( ¬ ¬ A ) ∨ (¬ A)
 -- mid-ex-neg {n} {A} = {!!}