---

Step * 1 1 of Lemma product-equipollent-tuple2


1. [A] : Type
2. L : Type List
3. L = [] ∈ (Type List)
⊢ A × Unit ~ A
BY
{ xxx((RWO "equipollent-product-com" 0 THENA Auto)
      THEN BLemma `equipollent-identity`
      THEN Auto
      THEN RelRST
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  L  :  Type  List
3.  L  =  []
\mvdash{}  A  \mtimes{}  Unit  \msim{}  A


By

---

Latex:
xxx((RWO  "equipollent-product-com"  0  THENA  Auto)
        THEN  BLemma  `equipollent-identity`
        THEN  Auto
        THEN  RelRST
        THEN  Auto)xxx

---

Home Index