---

Step * 2 1 of Lemma product-equipollent-tuple3

.....equality..... 
1. u : Type
2. v : Type List
3. ∀[A:Type]. tuple-type(v) × A ~ tuple-type(v @ [A])
4. A : Type
5. tuple-type(v) × A ~ tuple-type(v @ [A])
⊢ null(v @ [A]) ~ ff
BY
{ (DVar `v'  THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  u  :  Type
2.  v  :  Type  List
3.  \mforall{}[A:Type].  tuple-type(v)  \mtimes{}  A  \msim{}  tuple-type(v  @  [A])
4.  A  :  Type
5.  tuple-type(v)  \mtimes{}  A  \msim{}  tuple-type(v  @  [A])
\mvdash{}  null(v  @  [A])  \msim{}  ff


By

---

Latex:
(DVar  `v'    THEN  Reduce  0  THEN  Auto)

---

Home Index