---

Step * of Lemma append-tuple-one-one

∀[L1,L2:Type List].
  ∀[x1,x2:tuple-type(L1)]. ∀[y1,y2:tuple-type(L2)].
    {(x1 = x2 ∈ tuple-type(L1)) ∧ (y1 = y2 ∈ tuple-type(L2))} 
    supposing append-tuple(||L1||;||L2||;x1;y1) = append-tuple(||L1||;||L2||;x2;y2) ∈ tuple-type(L1 @ L2) 
  supposing 0 < ||L2||
BY
{ (Auto
   THEN (ApFunToHypEquands `Z' ⌜split-tuple(Z;||L1||)⌝ 
                                  ⌜tuple-type(firstn(||L1||;L1 @ L2)) × tuple-type(nth_tl(||L1||;L1 @ L2))⌝ (-1)⋅
         THENA (Auto THEN Auto')
         )
   THEN RWO "split-tuple-append-tuple" (-1)
   THEN Auto) }

1
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, y1> = <x2, y2> ∈ (tuple-type(firstn(||L1||;L1 @ L2)) × tuple-type(nth_tl(||L1||;L1 @ L2)))
⊢ {(x1 = x2 ∈ tuple-type(L1)) ∧ (y1 = y2 ∈ tuple-type(L2))}

---

Latex:

---

Latex:
\mforall{}[L1,L2:Type  List].
    \mforall{}[x1,x2:tuple-type(L1)].  \mforall{}[y1,y2:tuple-type(L2)].
        \{(x1  =  x2)  \mwedge{}  (y1  =  y2)\} 
        supposing  append-tuple(||L1||;||L2||;x1;y1)  =  append-tuple(||L1||;||L2||;x2;y2) 
    supposing  0  <  ||L2||


By

---

Latex:
(Auto
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}split-tuple(Z;||L1||)\mkleeneclose{} 
                                                                \mkleeneopen{}tuple-type(firstn(||L1||;L1  @  L2))  \mtimes{}  tuple-type(nth\_tl(||L1||;L1
                                                                                                                                                                                @  L2))\mkleeneclose{}  (-1)
              \mcdot{}
              THENA  (Auto  THEN  Auto')
              )
  THEN  RWO  "split-tuple-append-tuple"  (-1)
  THEN  Auto)

---

Home Index