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