---

Step * of Lemma product-equipollent-tuple3

∀L:Type List. ∀[A:Type]. tuple-type(L) × A ~ tuple-type(L @ [A])
BY
{ TACTIC:(InductionOnList THEN Reduce 0) }

1
∀[A:Type]. Unit × A ~ A

2
1. u : Type
2. v : Type List
3. ∀[A:Type]. tuple-type(v) × A ~ tuple-type(v @ [A])
⊢ ∀[A:Type]. if null(v) then u else u × tuple-type(v) fi  × A ~ if null(v @ [A]) then u else u × tuple-type(v @ [A]) fi 

---

Latex:

---

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


By

---

Latex:
TACTIC:(InductionOnList  THEN  Reduce  0)

---

Home Index