---

Step * 2 of Lemma assert-product-deq


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
BY
{ ((EqHD (-2) THENA Auto) THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:

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>
10.  x1  =  y1
\mvdash{}  x2  =  y2


By

---

Latex:
((EqHD  (-2)  THENA  Auto)  THEN  All  Reduce  THEN  Auto)

---

Home Index