---

Step * 2 1 of Lemma bag-map-no-repeats


1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ T2
4. bs : T1 List
5. Inj(T1;T2;f)
6. L : T1 List
7. no_repeats(T1;L)
8. L = bs ∈ bag(T1)
⊢ ∃L@0:T2 List. ((L@0 = map(f;L) ∈ bag(T2)) ∧ no_repeats(T2;L@0))
BY
{ (With ⌜map(f;L)⌝ (D 0)⋅
   THEN Try (Complete (Auto))
   THEN ((Fold `bag-map` 0 THEN Auto) THEN Unfold `bag-map` 0 THEN BLemma `no_repeats_map`  THEN Auto)⋅) }

1
1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ T2
4. bs : T1 List
5. Inj(T1;T2;f)
6. L : T1 List
7. no_repeats(T1;L)
8. L = bs ∈ bag(T1)
9. bag-map(f;L) = bag-map(f;L) ∈ bag(T2)
⊢ Inj({x:T1| (x ∈ L)} ;T2;f)

---

Latex:

---

Latex:

1.  T1  :  Type
2.  T2  :  Type
3.  f  :  T1  {}\mrightarrow{}  T2
4.  bs  :  T1  List
5.  Inj(T1;T2;f)
6.  L  :  T1  List
7.  no\_repeats(T1;L)
8.  L  =  bs
\mvdash{}  \mexists{}L@0:T2  List.  ((L@0  =  map(f;L))  \mwedge{}  no\_repeats(T2;L@0))


By

---

Latex:
(With  \mkleeneopen{}map(f;L)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  ((Fold  `bag-map`  0  THEN  Auto)  THEN  Unfold  `bag-map`  0  THEN  BLemma  `no\_repeats\_map`    THEN  Auto)
  \mcdot{})

---

Home Index