Step
*
2
2
1
of Lemma
tuple-type-append-equipollent
1. u : Type
2. v : Type List
3. ∀L2:Type List. tuple-type(v) × tuple-type(L2) ~ tuple-type(v @ L2)
4. L2 : Type List
5. v = [] ∈ (Type List)
6. ¬((v @ L2) = [] ∈ (Type List))
⊢ u × tuple-type(L2) ~ u × Unit × tuple-type(L2)
BY
{ Assert ⌜Unit × tuple-type(L2) ~ tuple-type(L2)⌝⋅ }
1
.....assertion.....
1. u : Type
2. v : Type List
3. ∀L2:Type List. tuple-type(v) × tuple-type(L2) ~ tuple-type(v @ L2)
4. L2 : Type List
5. v = [] ∈ (Type List)
6. ¬((v @ L2) = [] ∈ (Type List))
⊢ Unit × tuple-type(L2) ~ tuple-type(L2)
2
1. u : Type
2. v : Type List
3. ∀L2:Type List. tuple-type(v) × tuple-type(L2) ~ tuple-type(v @ L2)
4. L2 : Type List
5. v = [] ∈ (Type List)
6. ¬((v @ L2) = [] ∈ (Type List))
7. Unit × tuple-type(L2) ~ tuple-type(L2)
⊢ u × tuple-type(L2) ~ u × Unit × tuple-type(L2)
Latex:
Latex:
1. u : Type
2. v : Type List
3. \mforall{}L2:Type List. tuple-type(v) \mtimes{} tuple-type(L2) \msim{} tuple-type(v @ L2)
4. L2 : Type List
5. v = []
6. \mneg{}((v @ L2) = [])
\mvdash{} u \mtimes{} tuple-type(L2) \msim{} u \mtimes{} Unit \mtimes{} tuple-type(L2)
By
Latex:
Assert \mkleeneopen{}Unit \mtimes{} tuple-type(L2) \msim{} tuple-type(L2)\mkleeneclose{}\mcdot{}
Home
Index