---

Step * of Lemma assert-product-deq

∀[A,B:Type]. ∀[a:EqDecider(A)]. ∀[b:EqDecider(B)]. ∀[x,y:A × B].  uiff(↑(product-deq(A;B;a;b) x y);x = y ∈ (A × B))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``product-deq proddeq`` 0
   THEN DProdsAndUnions
   THEN Reduce 0
   THEN Auto
   THEN RW assert_pushdownC (-1)
   THEN Auto) }

1
1. A : Type
2. B : Type
3. a : EqDecider(A)
4. b : EqDecider(B)
5. x1 : A
6. x2 : B
7. y1 : A
8. y2 : B
9. <x1, x2> = <y1, y2> ∈ (A × B)
⊢ x1 = y1 ∈ A

2
1. A : Type
2. B : Type
3. a : EqDecider(A)
4. b : EqDecider(B)
5. x1 : A
6. x2 : B
7. y1 : A
8. y2 : B
9. <x1, x2> = <y1, y2> ∈ (A × B)
10. x1 = y1 ∈ A
⊢ x2 = y2 ∈ B

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[a:EqDecider(A)].  \mforall{}[b:EqDecider(B)].  \mforall{}[x,y:A  \mtimes{}  B].
    uiff(\muparrow{}(product-deq(A;B;a;b)  x  y);x  =  y)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``product-deq  proddeq``  0
  THEN  DProdsAndUnions
  THEN  Reduce  0
  THEN  Auto
  THEN  RW  assert\_pushdownC  (-1)
  THEN  Auto)

---

Home Index