---

Step * of Lemma tuple-type-valueall-type

∀[L:{T:Type| valueall-type(T)}  List]. valueall-type(tuple-type(L))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[L:\{T:Type|  valueall-type(T)\}    List].  valueall-type(tuple-type(L))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  AutoSplit)

---

Home Index