--- a/OPair.agda	Fri Jul 31 12:57:59 2020 +0900
+++ b/OPair.agda	Fri Jul 31 17:42:25 2020 +0900
@@ -166,10 +166,6 @@
     lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (od→ord < a , b >)
     lemma2 = replacement← A a A∋a
 
--- axiom of choice required
--- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFProduct (od→ord x)
--- ⊗⊆ZFP {A} {B} {x} lt = subst (λ k → ord-pair (od→ord k )) {!!} op-cons
-
 x<nextA : {A x : HOD} → A ∋ x →  od→ord x o< next (odmax A)
 x<nextA {A} {x} A∋x = ordtrans (c<→o< {x} {A} A∋x) ho<
 
@@ -201,21 +197,10 @@
        lemma p lt | pair x y | tri> ¬a ¬b c = ordtrans (ω-opair  (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y))))))
            (A<Bnext c (subst (λ k → odef B k ) (sym diso) (proj2 (proj2 lt (pair x y)))))) (omax-x _ _ ) 
 
-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 with union← AxB (ord→od x) (d→∋ (A ⊗ B) lt)
-      ... | t = {!!}
+ZFP⊆⊗ :  {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
+ZFP⊆⊗ {A} {B} {px} record { proj1 = (pair x y) ; proj2 = p2 } = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) )))
 
-
-
-
+-- axiom of choice required
+-- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFProduct (od→ord x)
+-- ⊗⊆ZFP {A} {B} {x} lt = subst (λ k → ord-pair (od→ord k )) {!!} op-cons
 
-
-
-
-