---

Step * of Lemma no_repeats_map_uiff

∀[T:Type]. ∀[L:T List]. ∀[A:Type]. ∀[f:{x:T| (x ∈ L)}  ⟶ A].
  uiff(no_repeats(A;map(f;L));no_repeats(T;L)) supposing Inj({x:T| (x ∈ L)} ;A;f)
BY
{ (Fold `mapl` 0 THEN Auto THEN Try ((Unfold `mapl` 0 THEN BLemma `no_repeats_map`  THEN Auto))) }

1
1. T : Type
2. L : T List
3. A : Type
4. f : {x:T| (x ∈ L)}  ⟶ A
5. Inj({x:T| (x ∈ L)} ;A;f)
6. no_repeats(A;mapl(f;L))
⊢ no_repeats(T;L)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[A:Type].  \mforall{}[f:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  A].
    uiff(no\_repeats(A;map(f;L));no\_repeats(T;L))  supposing  Inj(\{x:T|  (x  \mmember{}  L)\}  ;A;f)


By

---

Latex:
(Fold  `mapl`  0  THEN  Auto  THEN  Try  ((Unfold  `mapl`  0  THEN  BLemma  `no\_repeats\_map`    THEN  Auto)))

---

Home Index