---

Step * of Lemma bag-product_wf

∀[A,B:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)].  (as × bs ∈ bag(A × B))
BY
{ (Auto
   THEN (Assert ∀[as:A List]. ∀[bs:bag(B)].  (as × bs ∈ bag(A × B)) BY
               (InductionOnList
                THEN Auto
                THEN Unfold `bag-product` 0
                THEN Reduce 0
                THEN Auto
                THEN Fold `bag-product` 0
                THEN Auto))
   THEN (Assert λ2as.as × bs ∈ bag(A) ⟶ bag(A × B) BY
               (BLemma `bag-function`
                THEN Auto
                THEN ListInd (-2)
                THEN RepUR ``bag-product`` 0
                THEN Fold `bag-product` 0
                THEN Auto
                THEN HypSubst' (-1) 0
                THEN Auto
                THEN (InstHyp [⌜v⌝;⌜bs⌝] 5⋅ THENA Auto)
                THEN RWO "bag-append-assoc" 0
                THEN Auto))
   THEN (Subst' as × bs ~ λ2as.as × bs as 0 THENA (RepUR ``so_lambda`` 0 THEN Auto))) }

1
1. A : Type
2. B : Type
3. as : bag(A)
4. bs : bag(B)
5. ∀[as:A List]. ∀[bs:bag(B)].  (as × bs ∈ bag(A × B))
6. λ2as.as × bs ∈ bag(A) ⟶ bag(A × B)
⊢ λ2as.as × bs as ∈ bag(A × B)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[as:bag(A)].  \mforall{}[bs:bag(B)].    (as  \mtimes{}  bs  \mmember{}  bag(A  \mtimes{}  B))


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}[as:A  List].  \mforall{}[bs:bag(B)].    (as  \mtimes{}  bs  \mmember{}  bag(A  \mtimes{}  B))  BY
                          (InductionOnList
                            THEN  Auto
                            THEN  Unfold  `bag-product`  0
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  Fold  `bag-product`  0
                            THEN  Auto))
  THEN  (Assert  \mlambda{}\msubtwo{}as.as  \mtimes{}  bs  \mmember{}  bag(A)  {}\mrightarrow{}  bag(A  \mtimes{}  B)  BY
                          (BLemma  `bag-function`
                            THEN  Auto
                            THEN  ListInd  (-2)
                            THEN  RepUR  ``bag-product``  0
                            THEN  Fold  `bag-product`  0
                            THEN  Auto
                            THEN  HypSubst'  (-1)  0
                            THEN  Auto
                            THEN  (InstHyp  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
                            THEN  RWO  "bag-append-assoc"  0
                            THEN  Auto))
  THEN  (Subst'  as  \mtimes{}  bs  \msim{}  \mlambda{}\msubtwo{}as.as  \mtimes{}  bs  as  0  THENA  (RepUR  ``so\_lambda``  0  THEN  Auto)))

---

Home Index