---

Step * 1 of Lemma product-equipollent-tuple3


∀[A:Type]. Unit × A ~ A
BY
{ (Auto THEN BLemma `equipollent-identity` THEN Auto) }

---

Latex:

---

Latex:

\mforall{}[A:Type].  Unit  \mtimes{}  A  \msim{}  A


By

---

Latex:
(Auto  THEN  BLemma  `equipollent-identity`  THEN  Auto)

---

Home Index