---

Step * 2 of Lemma no_repeats_inject


1. T : Type
2. l : T List
3. ∀a1,a2:ℕ||l||.  ((((λi.l[i]) a1) = ((λi.l[i]) a2) ∈ T) ⇒ (a1 = a2 ∈ ℕ||l||))
4. i : ℕ
5. j : ℕ
6. i < ||l||
7. j < ||l||
8. ¬(i = j ∈ ℕ)
⊢ ¬(l[i] = l[j] ∈ T)
BY
{ (All Reduce THEN ParallelLast THEN Auto THEN BHyp 3  THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(All  Reduce  THEN  ParallelLast  THEN  Auto  THEN  BHyp  3    THEN  Auto)

---

Home Index