---

Step * 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
⊢ False
BY
{ (AllHyps (InstHyp [i1;i + ||l1||]) THEN Auto') }

1
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
12. ¬(l1 @ l2[i1] = l1 @ l2[i + ||l1||] ∈ T)
⊢ False

---

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{}  False


By

---

Latex:
(AllHyps  (InstHyp  [i1;i  +  ||l1||])  THEN  Auto')

---

Home Index