---

Step * 1 of Lemma bag-member-map


1. T : Type
2. U : Type
3. x : U
4. f : T ⟶ U
5. bs : bag(T)
6. x ↓∈ bag-map(f;bs)
⊢ ↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
BY
{ ((InstLemma `bag_to_squash_list` [⌜T⌝; ⌜bs⌝]⋅ THENA Auto)
   THEN SquashExRepD
   THEN MoveToConcl (-3)
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN Thin (-1)
   THEN Thin (-2)) }

1
1. T : Type
2. U : Type
3. x : U
4. f : T ⟶ U
5. L : T List
⊢ x ↓∈ bag-map(f;L) ⇒ (↓∃v:T. (v ↓∈ L ∧ (x = (f v) ∈ U)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  U  :  Type
3.  x  :  U
4.  f  :  T  {}\mrightarrow{}  U
5.  bs  :  bag(T)
6.  x  \mdownarrow{}\mmember{}  bag-map(f;bs)
\mvdash{}  \mdownarrow{}\mexists{}v:T.  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v)))


By

---

Latex:
((InstLemma  `bag\_to\_squash\_list`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SquashExRepD
  THEN  MoveToConcl  (-3)
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Thin  (-2))

---

Home Index