---

Step * of Lemma equipollent-identity-left

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

---

Latex:

---

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


By

---

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

---

Home Index