---

Step * 1 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. 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))} 
BY
{ TACTIC:((RWO "no_repeats_l_index" (-1)) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  no\_repeats(T;L)
5.  a1  :  T@i
6.  i1  :  \mBbbN{}@i
7.  i1  <  ||L||
8.  a1  =  L[i1]
9.  a2  :  T@i
10.  i  :  \mBbbN{}@i
11.  i  <  ||L||
12.  a2  =  L[i]
13.  index(L;L[i1])  =  index(L;L[i])
\mvdash{}  a1  =  a2


By

---

Latex:
TACTIC:((RWO  "no\_repeats\_l\_index"  (-1))  THEN  Auto)

---

Home Index