---

Step * 1 1 of Lemma append-tuple-one-one


1. L1 : Type List
2. L2 : Type List
3. 0 < ||L2||
4. x1 : tuple-type(L1)
5. x2 : tuple-type(L1)
6. y1 : tuple-type(L2)
7. y2 : tuple-type(L2)
8. append-tuple(||L1||;||L2||;x1;y1) = append-tuple(||L1||;||L2||;x2;y2) ∈ tuple-type(L1 @ L2)
9. x1 = x2 ∈ tuple-type(firstn(||L1||;L1 @ L2))
10. y1 = y2 ∈ tuple-type(nth_tl(||L1||;L1 @ L2))
⊢ x1 = x2 ∈ tuple-type(L1)
BY
{ (Subst' firstn(||L1||;L1 @ L2) ~ L1 -2 THEN Auto) }

---

Latex:

---

Latex:

1.  L1  :  Type  List
2.  L2  :  Type  List
3.  0  <  ||L2||
4.  x1  :  tuple-type(L1)
5.  x2  :  tuple-type(L1)
6.  y1  :  tuple-type(L2)
7.  y2  :  tuple-type(L2)
8.  append-tuple(||L1||;||L2||;x1;y1)  =  append-tuple(||L1||;||L2||;x2;y2)
9.  x1  =  x2
10.  y1  =  y2
\mvdash{}  x1  =  x2


By

---

Latex:
(Subst'  firstn(||L1||;L1  @  L2)  \msim{}  L1  -2  THEN  Auto)

---

Home Index