--- a/ordinal.agda	Tue Jul 16 09:57:01 2019 +0900
+++ b/ordinal.agda	Wed Jul 17 10:52:31 2019 +0900
@@ -321,21 +321,20 @@
 TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = 
       caseOSuc lx ox (TransFinite caseΦ caseOSuc  record { lv = lx ; ord = ox })
 
+-- we cannot prove this in intutonistic logic 
 --  (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )  → p
---      may be we can prove this...
-postulate 
- TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 
-  → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
-  → {p : Set l} ( P : { y : Ordinal {n} } →  ψ y → p )
-  → p
-
--- TransFiniteExists {n} {ψ} exists {p} P = ⊥-elim ( exists lemma ) where
---     lemma : (y : Ordinal {n} ) → ¬ ψ y
---     lemma y ψy = ( TransFinite {n} {{!!}} {!!} {!!} y ) ψy
-TransFiniteExists' : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 
+-- postulate 
+--  TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 
+--   → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
+--   → {p : Set l} ( P : { y : Ordinal {n} } →  ψ y → p )
+--   → p
+--
+-- Instead we prove
+--
+TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 
   → {p : Set l} ( P : { y : Ordinal {n} } →  ψ y → ¬ p )
   → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
   → ¬ p
-TransFiniteExists' {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
+TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )