---

Step * 1 1 of Lemma no_repeats_l_index-inj


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. no_repeats(T;L)
5. a1 : T@i
6. (a1 ∈ L)
7. a2 : T@i
8. (a2 ∈ L)
9. index(L;a1) = index(L;a2) ∈ ℕ||L||
⊢ a1 = a2 ∈ {x:T| (x ∈ L)} 
BY
{ TACTIC:((All (Unfold `l_member`))
          THEN ExRepD
          THEN ((StrongHypSubst 8 (-1)) THENA (D -1 THEN Auto THEN HypSubst' -1 0 THEN Auto))
          THEN ((StrongHypSubst 12 (-1)) THENA (D -1 THEN Auto THEN HypSubst' -1 0 THEN Auto))) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. no_repeats(T;L)
5. a1 : T@i
6. i1 : ℕ@i
7. i1 < ||L||
8. a1 = L[i1] ∈ T
9. a2 : T@i
10. i : ℕ@i
11. i < ||L||
12. a2 = L[i] ∈ T
13. index(L;L[i1]) = index(L;L[i]) ∈ ℕ||L||
⊢ a1 = a2 ∈ {x:T| ∃i:ℕ. (i < ||L|| c∧ (x = L[i] ∈ T))} 

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  no\_repeats(T;L)
5.  a1  :  T@i
6.  (a1  \mmember{}  L)
7.  a2  :  T@i
8.  (a2  \mmember{}  L)
9.  index(L;a1)  =  index(L;a2)
\mvdash{}  a1  =  a2


By

---

Latex:
TACTIC:((All  (Unfold  `l\_member`))
                THEN  ExRepD
                THEN  ((StrongHypSubst  8  (-1))  THENA  (D  -1  THEN  Auto  THEN  HypSubst'  -1  0  THEN  Auto))
                THEN  ((StrongHypSubst  12  (-1))  THENA  (D  -1  THEN  Auto  THEN  HypSubst'  -1  0  THEN  Auto)))

---

Home Index