---

Step * 1 of Lemma tuple-type-concat


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)]))
BY
{ TACTIC:(Unfold `concat` 0 THEN Reduce 0 THEN Fold `concat` 0) }

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((f u) @ concat(map(f;v)))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  T  {}\mrightarrow{}  (Type  List)
3.  u  :  T
4.  v  :  T  List
5.  tuple-type(map(\mlambda{}i.tuple-type(f  i);v))  \msim{}  tuple-type(concat(map(f;v)))
\mvdash{}  if  null(map(\mlambda{}i.tuple-type(f  i);v))
then  tuple-type(f  u)
else  tuple-type(f  u)  \mtimes{}  tuple-type(map(\mlambda{}i.tuple-type(f  i);v))
fi    \msim{}  tuple-type(concat([f  u  /  map(f;v)]))


By

---

Latex:
TACTIC:(Unfold  `concat`  0  THEN  Reduce  0  THEN  Fold  `concat`  0)

---

Home Index