---

Step * 1 of Lemma bag-product-no-repeats


1. A : Type
2. B : Type
3. bag-no-repeats(A;[])
4. bs : bag(B)
5. bag-no-repeats(B;bs)
⊢ bag-no-repeats(A × B;[] × bs)
BY
{ (Folds ``empty-bag`` 0 THEN RWO "bag-product-empty" 0 THEN Auto THEN BLemma `empty-bag-no-repeats` THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  bag-no-repeats(A;[])
4.  bs  :  bag(B)
5.  bag-no-repeats(B;bs)
\mvdash{}  bag-no-repeats(A  \mtimes{}  B;[]  \mtimes{}  bs)


By

---

Latex:
(Folds  ``empty-bag``  0
  THEN  RWO  "bag-product-empty"  0
  THEN  Auto
  THEN  BLemma  `empty-bag-no-repeats`
  THEN  Auto)\mcdot{}

---

Home Index