---

Step * of Lemma bag-map-list-map

∀[T,U:Type].  ∀L1:T List. ∀L2:U List. ∀f:T ⟶ U.  ((L2 = map(f;L1) ∈ bag(U)) ⇒ (∃L:U List. (L = map(f;L1) ∈ (U List))))
BY
{ (Auto THEN InstConcl [⌜map(f;L1)⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,U:Type].    \mforall{}L1:T  List.  \mforall{}L2:U  List.  \mforall{}f:T  {}\mrightarrow{}  U.    ((L2  =  map(f;L1))  {}\mRightarrow{}  (\mexists{}L:U  List.  (L  =  map(f;L1))))


By

---

Latex:
(Auto  THEN  InstConcl  [\mkleeneopen{}map(f;L1)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index