# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1596167879 -32400
# Node ID 4af94768e3725c8bf4850f30dd7f7fc0fc7d0394
# Parent  f6f08d5a49410cea46855b6304a5a3915d51421e
...

diff -r f6f08d5a4941 -r 4af94768e372 OPair.agda
--- a/OPair.agda	Fri Jul 31 12:46:45 2020 +0900
+++ b/OPair.agda	Fri Jul 31 12:57:59 2020 +0900
@@ -203,12 +203,13 @@
 
 ZFP⊗ :  {A B : HOD} → ZFP A B ≡ A ⊗ B
 ZFP⊗ {A} {B} = ==→o≡ record { eq→ = lemma0 ; eq← = lemma1 } where
+      AxB : HOD
+      AxB =  Replace B (λ b → Replace A (λ a → < a , b > )) 
       lemma0 :  {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
       lemma0 {px} record { proj1 = (pair x y) ; proj2 = p2 } = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) )))
       lemma1 :  {x : Ordinal} → odef (A ⊗ B) x → odef (ZFP A B) x
-      lemma1 {x} lt = ⊥-elim (lt (λ u not → proj2 (proj1 not) (λ y p → lemma2 u y p ))) where
-           lemma2 : (u y : Ordinal) → odef B y ∧ (u ≡ od→ord (Replace A (λ a → < a , ord→od y >))) → ⊥
-           lemma2 = {!!}
+      lemma1 {x} lt with union← AxB (ord→od x) (d→∋ (A ⊗ B) lt)
+      ... | t = {!!}
 
 
 
diff -r f6f08d5a4941 -r 4af94768e372 ordinal.agda
--- a/ordinal.agda	Fri Jul 31 12:46:45 2020 +0900
+++ b/ordinal.agda	Fri Jul 31 12:57:59 2020 +0900
@@ -244,7 +244,6 @@
          lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where
              lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥
              lemma3   (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n
-
      open Oprev
      Oprev-p  : (x : Ordinal) → Dec ( Oprev (Ordinal {suc n})  osuc x )
      Oprev-p  (ordinal lv (Φ lv)) = no (λ not → lemma (oprev not) (oprev=x not) ) where