--- a/OD.agda	Mon Jul 22 18:36:45 2019 +0900
+++ b/OD.agda	Mon Jul 22 18:49:38 2019 +0900
@@ -292,7 +292,7 @@
        ;   empty = empty
        ;   power→ = power→  
        ;   power← = power← 
-       ;   extensionality = extensionality
+       ;   extensionality = λ {A} {B} {w} → extensionality {A} {B} {w} 
        ;   ε-induction = ε-induction
        ;   infinity∅ = infinity∅
        ;   infinity = infinity
@@ -441,9 +441,13 @@
              lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁
              lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {suc n} {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) ))
 
-         extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
-         eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
-         eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
+         extensionality0 : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
+         eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
+         eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
+
+         extensionality : {A B w : OD {suc n} } → ((z : OD {suc n}) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
+         proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
+         proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d 
 
          infinity∅ : infinite  ∋ od∅ {suc n}
          infinity∅ = def-subst {suc n} {_} {_} {infinite} {od→ord (od∅ {suc n})} iφ refl lemma where