---

Step * of Lemma sub-bag-map-equal

∀[T,U:Type]. ∀[b1,b2:bag(T)]. ∀[f:T ⟶ U].
  (b1 = b2 ∈ bag(T)) supposing (sub-bag(T;b2;b1) and sub-bag(U;bag-map(f;b1);bag-map(f;b2)))
BY
{ ((UnivCD THENA Auto)
   THEN All (Unfold `sub-bag`)
   THEN ExRepD
   THEN (HypSubst' (-1) (-3) THENA Auto)
   THEN (HypSubst' (-2) 0 THENA Auto)
   THEN ThinVar `b1'
   THEN (Assert ⌜cs = {} ∈ bag(T)⌝⋅ THENM ((HypSubst' (-1) 0 THENA Auto) THEN RWO "bag-append-empty" 0 THEN Auto))
   THEN (BagToList 3 THENA Auto)
   THEN (BagToList (-3) THENA Auto)
   THEN (BagToList (-2) THENA Auto)
   THEN RepUR ``bag-append bag-map`` (-1)
   THEN RepUR ``empty-bag`` 0
   THEN (RWO "map_append_sq" (-1) THENA Auto)) }

1
1. T : Type
2. U : Type
3. b2 : T List
4. f : T ⟶ U
5. c1 : U List
6. cs : T List
7. map(f;b2) = ((map(f;b2) @ map(f;cs)) @ c1) ∈ bag(U)
⊢ cs = [] ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T,U:Type].  \mforall{}[b1,b2:bag(T)].  \mforall{}[f:T  {}\mrightarrow{}  U].
    (b1  =  b2)  supposing  (sub-bag(T;b2;b1)  and  sub-bag(U;bag-map(f;b1);bag-map(f;b2)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  All  (Unfold  `sub-bag`)
  THEN  ExRepD
  THEN  (HypSubst'  (-1)  (-3)  THENA  Auto)
  THEN  (HypSubst'  (-2)  0  THENA  Auto)
  THEN  ThinVar  `b1'
  THEN  (Assert  \mkleeneopen{}cs  =  \{\}\mkleeneclose{}\mcdot{}
  THENM  ((HypSubst'  (-1)  0  THENA  Auto)  THEN  RWO  "bag-append-empty"  0  THEN  Auto)
  )
  THEN  (BagToList  3  THENA  Auto)
  THEN  (BagToList  (-3)  THENA  Auto)
  THEN  (BagToList  (-2)  THENA  Auto)
  THEN  RepUR  ``bag-append  bag-map``  (-1)
  THEN  RepUR  ``empty-bag``  0
  THEN  (RWO  "map\_append\_sq"  (-1)  THENA  Auto))

---

Home Index