--- a/ordinal.agda	Mon Jul 08 12:34:08 2019 +0900
+++ b/ordinal.agda	Mon Jul 08 13:21:14 2019 +0900
@@ -314,11 +314,14 @@
       caseOSuc lx ox (TransFinite caseΦ caseOSuc  record { lv = lx ; ord = ox })
 
 --  (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )  → p
-TransFiniteExists : {n : Level} → { ψ : Ordinal {n} → Set n } 
+--      may be we can prove this...
+postulate 
+ TransFiniteExists : {n : Level} → { ψ : Ordinal {n} → Set n } 
   → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
   → {p : Set n} ( 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} {ψ} exists {p} P = ⊥-elim ( exists lemma ) where
+--     lemma : (y : Ordinal {n} ) → ¬ ψ y
+--     lemma y ψy = ( TransFinite {n} {{!!}} {!!} {!!} y ) ψy