--- a/OD.agda	Thu Sep 05 10:58:06 2019 +0900
+++ b/OD.agda	Tue Sep 17 09:29:27 2019 +0900
@@ -350,6 +350,17 @@
     ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt }
    } 
 
+open import Data.Unit
+
+ε-induction : { ψ : OD  → Set (suc n)}
+   → ( {x : OD } → ({ y : OD } →  x ∋ y → ψ y ) → ψ x )
+   → (x : OD ) → ψ x
+ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
+     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
+     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 
+     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
+     ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
+
 OD→ZF : ZF  
 OD→ZF   = record { 
     ZFSet = OD