---

Step * of Lemma tuple-type-concat

∀[T:Type]. ∀f:T ⟶ (Type List). ∀L:T List.  tuple-type(map(λi.tuple-type(f i);L)) ~ tuple-type(concat(map(f;L)))
BY
{ TACTIC:(InductionOnList THEN Reduce 0 THEN Auto) }

1
1. [T] : Type
2. f : T ⟶ (Type List)
3. u : T
4. v : T List
5. tuple-type(map(λi.tuple-type(f i);v)) ~ tuple-type(concat(map(f;v)))
⊢ if null(map(λi.tuple-type(f i);v))
then tuple-type(f u)
else tuple-type(f u) × tuple-type(map(λi.tuple-type(f i);v))
fi  ~ tuple-type(concat([f u / map(f;v)]))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}f:T  {}\mrightarrow{}  (Type  List).  \mforall{}L:T  List.
        tuple-type(map(\mlambda{}i.tuple-type(f  i);L))  \msim{}  tuple-type(concat(map(f;L)))


By

---

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

---

Home Index