---

Step * of Lemma product-equipollent-tuple2

∀[A:Type]. ∀L:Type List. A × tuple-type(L) ~ tuple-type([A / L])
BY
{ (Reduce 0 THEN Auto THEN AutoSplit THEN Try ((RelRST THEN Auto))) }

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

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}L:Type  List.  A  \mtimes{}  tuple-type(L)  \msim{}  tuple-type([A  /  L])


By

---

Latex:
(Reduce  0  THEN  Auto  THEN  AutoSplit  THEN  Try  ((RelRST  THEN  Auto)))

---

Home Index