---

Step * 1 of Lemma no_repeats_l_index-inj


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. no_repeats(T;L)
⊢ Inj({x:T| (x ∈ L)} ;ℕ||L||;λx.index(L;x))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN Reduce 0
   THEN DVar `a1'
   THEN DVar `a2'
   THEN (All (RW assert_pushdownC))
   THEN Auto)⋅ }

1
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)} 

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  no\_repeats(T;L)
\mvdash{}  Inj(\{x:T|  (x  \mmember{}  L)\}  ;\mBbbN{}||L||;\mlambda{}x.index(L;x))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Reduce  0
  THEN  DVar  `a1'
  THEN  DVar  `a2'
  THEN  (All  (RW  assert\_pushdownC))
  THEN  Auto)\mcdot{}

---

Home Index