---

Step * 1 of Lemma equipollent-product-com


1. A : Type
2. B : Type
3. a1 : A × B@i
4. a2 : A × B@i
5. let a,b = a1 in <b, a> = let a,b = a2 in <b, a> ∈ (B × A)@i
⊢ a1 = a2 ∈ (A × B)
BY
{ (D (-3) THEN D -2 THEN Reduce (-1) THEN EqHD (-1) THEN Auto THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  a1  :  A  \mtimes{}  B@i
4.  a2  :  A  \mtimes{}  B@i
5.  let  a,b  =  a1  in  <b,  a>  =  let  a,b  =  a2  in  <b,  a>@i
\mvdash{}  a1  =  a2


By

---

Latex:
(D  (-3)  THEN  D  -2  THEN  Reduce  (-1)  THEN  EqHD  (-1)  THEN  Auto  THEN  All  Reduce  THEN  Auto)

---

Home Index