---

Step * 1 1 1 of Lemma no_repeats_append


1. T : Type
2. l1 : T List
3. l2 : T List
4. ∀[i,j:ℕ].  (¬(l1 @ l2[i] = l1 @ l2[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||l1 @ l2|| and i < ||l1 @ l2||)
5. x : T
6. i1 : ℕ
7. i1 < ||l1||
8. x = l1[i1] ∈ T
9. i : ℕ
10. i < ||l2||
11. x = l2[i] ∈ T
⊢ x = l1 @ l2[i + ||l1||] ∈ T
BY
{ (((RWO "select_append_back" 0 THEN Auto') THEN RW IntNormC 0) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  l1  :  T  List
3.  l2  :  T  List
4.  \mforall{}[i,j:\mBbbN{}].
          (\mneg{}(l1  @  l2[i]  =  l1  @  l2[j]))  supposing  ((\mneg{}(i  =  j))  and  j  <  ||l1  @  l2||  and  i  <  ||l1  @  l2||)
5.  x  :  T
6.  i1  :  \mBbbN{}
7.  i1  <  ||l1||
8.  x  =  l1[i1]
9.  i  :  \mBbbN{}
10.  i  <  ||l2||
11.  x  =  l2[i]
\mvdash{}  x  =  l1  @  l2[i  +  ||l1||]


By

---

Latex:
(((RWO  "select\_append\_back"  0  THEN  Auto')  THEN  RW  IntNormC  0)  THEN  Auto)

---

Home Index