---

Step * 2 2 of Lemma product-equipollent-tuple3


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])
⊢ if null(v) then u else u × tuple-type(v) fi  × A ~ if ff then u else u × tuple-type(v @ [A]) fi 
BY
{ AutoSplit }

1
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])
6. v = [] ∈ (Type List)
⊢ u × A ~ u × tuple-type(v @ [A])

2
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.  \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{}  if  null(v)  then  u  else  u  \mtimes{}  tuple-type(v)  fi    \mtimes{}  A  \msim{}  if  ff  then  u  else  u  \mtimes{}  tuple-type(v  @  [A])  fi 


By

---

Latex:
AutoSplit

---

Home Index