---

Step * 2 of Lemma product-equipollent-tuple3


1. u : Type
2. v : Type List
3. ∀[A:Type]. tuple-type(v) × A ~ tuple-type(v @ [A])
⊢ ∀[A:Type]. if null(v) then u else u × tuple-type(v) fi  × A ~ if null(v @ [A]) then u else u × tuple-type(v @ [A]) fi 
BY
{ TACTIC:(ParallelLast THEN Subst' null(v @ [A]) ~ ff 0) }

1
.....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

2
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 

---

Latex:

---

Latex:

1.  u  :  Type
2.  v  :  Type  List
3.  \mforall{}[A:Type].  tuple-type(v)  \mtimes{}  A  \msim{}  tuple-type(v  @  [A])
\mvdash{}  \mforall{}[A:Type]
        if  null(v)  then  u  else  u  \mtimes{}  tuple-type(v)  fi    \mtimes{}  A  \msim{}  if  null(v  @  [A])
        then  u
        else  u  \mtimes{}  tuple-type(v  @  [A])
        fi 


By

---

Latex:
TACTIC:(ParallelLast  THEN  Subst'  null(v  @  [A])  \msim{}  ff  0)

---

Home Index