Step
*
2
2
2
of Lemma
product-equipollent-tuple3
1. u : Type
2. v : Type List
3. ¬(v = [] ∈ (Type List))
4. ∀[A:Type]. tuple-type(v) × A ~ tuple-type(v @ [A])
5. [A] : Type
6. tuple-type(v) × A ~ tuple-type(v @ [A])
⊢ u × tuple-type(v) × A ~ u × tuple-type(v @ [A])
BY
{ (RWO "-1<" 0 THEN Auto) }
1
1. u : Type
2. v : Type List
3. ¬(v = [] ∈ (Type List))
4. ∀[A:Type]. tuple-type(v) × A ~ tuple-type(v @ [A])
5. [A] : Type
6. tuple-type(v) × A ~ tuple-type(v @ [A])
⊢ u × tuple-type(v) × A ~ u × tuple-type(v) × A
Latex:
Latex:
1.  u  :  Type
2.  v  :  Type  List
3.  \mneg{}(v  =  [])
4.  \mforall{}[A:Type].  tuple-type(v)  \mtimes{}  A  \msim{}  tuple-type(v  @  [A])
5.  [A]  :  Type
6.  tuple-type(v)  \mtimes{}  A  \msim{}  tuple-type(v  @  [A])
\mvdash{}  u  \mtimes{}  tuple-type(v)  \mtimes{}  A  \msim{}  u  \mtimes{}  tuple-type(v  @  [A])
By
Latex:
(RWO  "-1<"  0  THEN  Auto)
Home
Index