--- a/ordinal.agda	Thu Aug 15 04:51:24 2019 +0900
+++ b/ordinal.agda	Fri Aug 16 15:53:29 2019 +0900
@@ -204,21 +204,6 @@
       lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) 
       lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1
 
--- we cannot prove this in intutionistic logic 
---  (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )  → p
--- 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 ) 
 
 open import Ordinals