--- a/OD.agda	Tue Jul 23 11:08:24 2019 +0900
+++ b/OD.agda	Thu Jul 25 13:11:21 2019 +0900
@@ -191,6 +191,22 @@
 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () )
 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ())
 
+ppp : { n : Level } → { p : Set (suc n) } { a : OD {suc n} } → record { def = λ x → p } ∋ a → p
+ppp {n} {p} {a} d = d
+
+p∨¬p : { n : Level } → { p : Set (suc n) } → p ∨ ( ¬ p )
+p∨¬p {n} {p} with record { def = λ x → p } | record { def = λ x → ¬ p }  
+... | ps | ¬ps with is-o∅ ( od→ord ps)
+p∨¬p {n} {p} | ps | ¬ps | yes eq = case2 (¬p eq) where
+   ¬p : {ps1 : Ordinal {suc n}} → ( ps1  ≡ o∅ {suc n} ) → p → ⊥
+   ¬p refl = {!!}
+p∨¬p {n} {p} | ps | ¬ps | no ¬p = case1 (ppp {n} {p} {minimul ps (λ eq →  ¬p (eqo∅ eq))} (
+       def-subst {suc n} {ps} {_} {record { def = λ x → p }} {od→ord (minimul ps (λ eq →  ¬p (eqo∅ eq)))} lemma {!!} refl )) where
+   eqo∅ : ps ==  od∅ {suc n} → od→ord ps ≡  o∅ {suc n} 
+   eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) 
+   lemma : ps ∋ minimul ps (λ eq →  ¬p (eqo∅ eq)) 
+   lemma = x∋minimul ps (λ eq →  ¬p (eqo∅ eq))
+
 OrdP : {n : Level} →  ( x : Ordinal {suc n} ) ( y : OD {suc n} ) → Dec ( Ord x ∋ y )
 OrdP {n} x y with trio< x (od→ord y)
 OrdP {n} x y | tri< a ¬b ¬c = no ¬c
@@ -458,6 +474,8 @@
          choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 
          choice X {A} X∋A not = x∋minimul A not
 
+         -- choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD {suc n}
+
          -- another form of regularity 
          --
          ε-induction : {n m : Level} { ψ : OD {suc n} → Set m}

--- a/zf.agda	Tue Jul 23 11:08:24 2019 +0900
+++ b/zf.agda	Thu Jul 25 13:11:21 2019 +0900
@@ -21,6 +21,8 @@
 
 open import Relation.Nullary
 open import Relation.Binary
+open import Data.Empty
+
 
 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A 
 contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a ) 
@@ -28,6 +30,16 @@
 double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
 double-neg A notnot = notnot A
 
+double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
+double-neg2 notnot A = notnot ( double-neg A )
+
+de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
+de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
+de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
+
+-- mid-ex-neg : {n  : Level } {A : Set n} → ( ¬ ¬ A ) ∨ (¬ A)
+-- mid-ex-neg {n} {A} = {!!}
+
 infixr  130 _∧_
 infixr  140 _∨_
 infixr  150 _⇔_