---

Step * 1 of Lemma bag-combine-eq-right


1. A : Type
2. B : Type
3. b : A List
4. f1 : A ⟶ bag(B)
5. f2 : A ⟶ bag(B)
6. ∀x:{x:A| x ↓∈ b} . (f1[x] = f2[x] ∈ bag(B))
⊢ map(λx.f1[x];b) = map(λx.f2[x];b) ∈ bag(bag(B))
BY
{ ((Assert ⌜map(λx.f1[x];b) = map(λx.f2[x];b) ∈ (bag(B) List)⌝⋅ THENM (HypSubst' (-1) 0 THEN Auto))
   THEN BLemma `map_equal`
   THEN Auto
   THEN RepUR ``so_apply`` 0
   THEN InstHyp [⌜b[i]⌝] (-3)⋅
   THEN Try (Complete (Auto))
   THEN MemTypeCD
   THEN Auto
   THEN (BLemma `list-member-bag-member` THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  b  :  A  List
4.  f1  :  A  {}\mrightarrow{}  bag(B)
5.  f2  :  A  {}\mrightarrow{}  bag(B)
6.  \mforall{}x:\{x:A|  x  \mdownarrow{}\mmember{}  b\}  .  (f1[x]  =  f2[x])
\mvdash{}  map(\mlambda{}x.f1[x];b)  =  map(\mlambda{}x.f2[x];b)


By

---

Latex:
((Assert  \mkleeneopen{}map(\mlambda{}x.f1[x];b)  =  map(\mlambda{}x.f2[x];b)\mkleeneclose{}\mcdot{}  THENM  (HypSubst'  (-1)  0  THEN  Auto))
  THEN  BLemma  `map\_equal`
  THEN  Auto
  THEN  RepUR  ``so\_apply``  0
  THEN  InstHyp  [\mkleeneopen{}b[i]\mkleeneclose{}]  (-3)\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  MemTypeCD
  THEN  Auto
  THEN  (BLemma  `list-member-bag-member`  THEN  Auto)\mcdot{})

---

Home Index