---

Step * 1 of Lemma no_repeats_inject


1. T : Type
2. l : T List
3. ∀[i,j:ℕ].  (¬(l[i] = l[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||l|| and i < ||l||)
4. a1 : ℕ||l||
5. a2 : ℕ||l||
6. l[a1] = l[a2] ∈ T
⊢ a1 = a2 ∈ ℕ||l||
BY
{ (SupposeNot THEN (Assert ¬(l[a1] = l[a2] ∈ T) BY (BackThruSomeHyp THEN Auto)) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  l  :  T  List
3.  \mforall{}[i,j:\mBbbN{}].    (\mneg{}(l[i]  =  l[j]))  supposing  ((\mneg{}(i  =  j))  and  j  <  ||l||  and  i  <  ||l||)
4.  a1  :  \mBbbN{}||l||
5.  a2  :  \mBbbN{}||l||
6.  l[a1]  =  l[a2]
\mvdash{}  a1  =  a2


By

---

Latex:
(SupposeNot  THEN  (Assert  \mneg{}(l[a1]  =  l[a2])  BY  (BackThruSomeHyp  THEN  Auto))  THEN  Auto)

---

Home Index