---

Step * of Lemma no_repeats_inject

∀[T:Type]. ∀[l:T List].  uiff(no_repeats(T;l);Inj(ℕ||l||;T;λi.l[i]))
BY
{ ((UniformUnivCD Auto THENA Try (Complete (Auto)))
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN RepeatFor 2 (D 0)
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN (UnfoldTopAb (-1) THEN D 0 THEN Reduce 0 THEN Auto)⋅) }

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

2
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)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].    uiff(no\_repeats(T;l);Inj(\mBbbN{}||l||;T;\mlambda{}i.l[i]))


By

---

Latex:
((UniformUnivCD  Auto  THENA  Try  (Complete  (Auto)))
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  RepeatFor  2  (D  0)
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  (UnfoldTopAb  (-1)  THEN  D  0  THEN  Reduce  0  THEN  Auto)\mcdot{})

---

Home Index