---

Step * 1 of Lemma product-equipollent-tuple2


1. [A] : Type
2. L : Type List
3. L = [] ∈ (Type List)
⊢ A × tuple-type(L) ~ A
BY
{ (HypSubst' (-1) 0 THEN Reduce 0) }

1
1. [A] : Type
2. L : Type List
3. L = [] ∈ (Type List)
⊢ A × Unit ~ A

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  L  :  Type  List
3.  L  =  []
\mvdash{}  A  \mtimes{}  tuple-type(L)  \msim{}  A


By

---

Latex:
(HypSubst'  (-1)  0  THEN  Reduce  0)

---

Home Index