# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1567062526 -32400
# Node ID 0446b6c5e7bcbd1e7392316f0b80537ef47eecf9
# Parent  8a58e2cd1f55393e495c662f3ee7fea9be3e512e
proudct uniquness done

diff -r 8a58e2cd1f55 -r 0446b6c5e7bc cardinal.agda
--- a/cardinal.agda	Thu Aug 29 03:03:04 2019 +0900
+++ b/cardinal.agda	Thu Aug 29 16:08:46 2019 +0900
@@ -125,8 +125,12 @@
 p-iso1 :  { ox oy  : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >  
 p-iso1 {ox} {oy} = pair ox oy
 
-postulate
-    p-iso :  { x  : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
+p-iso :  { x  : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
+p-iso {x} p = ord≡→≡ (lemma2 p) where
+    lemma :  { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
+    lemma (pair ox oy) = refl
+    lemma2 : { x  : OD } → (p : ZFProduct ∋ x ) → od→ord < ord→od (π1 p) , ord→od (π2 p) > ≡ od→ord x
+    lemma2 {x} p = lemma p
 
     
 ∋-p : (A x : OD ) → Dec ( A ∋ x )