---

Step * of Lemma no_repeats_l_index-inj

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List].  Inj({x:T| (x ∈ L)} ;ℕ||L||;λx.index(L;x)) supposing no_repeats(T;L)
BY
{ TACTIC:(UniformUnivCD Auto THEN Try (Complete (Auto))) }

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].
    Inj(\{x:T|  (x  \mmember{}  L)\}  ;\mBbbN{}||L||;\mlambda{}x.index(L;x))  supposing  no\_repeats(T;L)


By

---

Latex:
TACTIC:(UniformUnivCD  Auto  THEN  Try  (Complete  (Auto)))

---

Home Index