---

Step * of Lemma bag-map-trivial

∀[A:Type]. ∀[as:bag(A)]. ∀[f:A ⟶ A].  bag-map(f;as) = as ∈ bag(A) supposing ∀x:A. ((f x) = x ∈ A)
BY
{ ((UnivCD THENA Auto)
   THEN BagD 2
   THEN Auto
   THEN (Assert as = bs ∈ bag(A) BY
               (EqTypeCD THEN Auto))
   THEN HypSubst'(-1) 0
   THEN Auto) }

1
1. A : Type
2. f : A ⟶ A
3. ∀x:A. ((f x) = x ∈ A)
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
7. as = bs ∈ bag(A)
⊢ bag-map(f;bs) = bs ∈ bag(A)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[as:bag(A)].  \mforall{}[f:A  {}\mrightarrow{}  A].    bag-map(f;as)  =  as  supposing  \mforall{}x:A.  ((f  x)  =  x)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  BagD  2
  THEN  Auto
  THEN  (Assert  as  =  bs  BY
                          (EqTypeCD  THEN  Auto))
  THEN  HypSubst'(-1)  0
  THEN  Auto)

---

Home Index