---

Step * 2 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
⊢ if null(v) then u else u × tuple-type(v) fi  × tuple-type(L2) ~ if null(v @ L2) then u else u × tuple-type(v @ L2) fi 
BY
{ (RepeatFor 2 (OldAutoSplit) THEN Try ((RWO "3<" 0 THEN Auto))⋅) }

1
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

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))
⊢ u × tuple-type(L2) ~ u × tuple-type(v) × tuple-type(L2)

3
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(v) × tuple-type(L2) ~ u × tuple-type(v) × 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
\mvdash{}  if  null(v)  then  u  else  u  \mtimes{}  tuple-type(v)  fi    \mtimes{}  tuple-type(L2)  \msim{}  if  null(v  @  L2)
then  u
else  u  \mtimes{}  tuple-type(v  @  L2)
fi 


By

---

Latex:
(RepeatFor  2  (OldAutoSplit)  THEN  Try  ((RWO  "3<"  0  THEN  Auto))\mcdot{})

---

Home Index