---

Step * 1 1 1 of Lemma tuple-type-concat

.....truecase..... 
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)))
6. map(λi.tuple-type(f i);v) = [] ∈ (Type List)
⊢ tuple-type(f u) ~ tuple-type((f u) @ concat(map(f;v)))
BY
{ (DVar `v' THEN All Reduce) }

1
1. [T] : Type
2. f : T ⟶ (Type List)
3. u : T
4. Unit ~ Unit
5. [] = [] ∈ (Type List)
⊢ tuple-type(f u) ~ tuple-type((f u) @ [])

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

---

Latex:

---

Latex:
.....truecase..... 
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)))
6.  map(\mlambda{}i.tuple-type(f  i);v)  =  []
\mvdash{}  tuple-type(f  u)  \msim{}  tuple-type((f  u)  @  concat(map(f;v)))


By

---

Latex:
(DVar  `v'  THEN  All  Reduce)

---

Home Index