---

Step * 2 1 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
5. v = [] ∈ (Type List)
6. (v @ L2) = [] ∈ (Type List)
⊢ u × tuple-type(L2) ~ u
BY
{ ((RWO "append_is_nil" (-1) THENM D -1) THENA 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 = [] ∈ (Type List)
7. L2 = [] ∈ (Type List)
⊢ u × tuple-type(L2) ~ u

---

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
5.  v  =  []
6.  (v  @  L2)  =  []
\mvdash{}  u  \mtimes{}  tuple-type(L2)  \msim{}  u


By

---

Latex:
((RWO  "append\_is\_nil"  (-1)  THENM  D  -1)  THENA  Auto)

---

Home Index