---

Step * 1 of Lemma null-bag-filter-map

.....wf..... 
1. T : Type
2. A : Type
3. f : A ⟶ T
4. p : T ⟶ 𝔹
5. as : A List
6. bs : A List
7. permutation(A;as;bs)
8. z : bag(A)
⊢ null(filter(λx.p[f x];z)) = null(filter(λx.p[f x];bs)) ∈ ℙ
BY
{ (Folds ``bag-filter bag-null`` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
2.  A  :  Type
3.  f  :  A  {}\mrightarrow{}  T
4.  p  :  T  {}\mrightarrow{}  \mBbbB{}
5.  as  :  A  List
6.  bs  :  A  List
7.  permutation(A;as;bs)
8.  z  :  bag(A)
\mvdash{}  null(filter(\mlambda{}x.p[f  x];z))  =  null(filter(\mlambda{}x.p[f  x];bs))  \mmember{}  \mBbbP{}


By

---

Latex:
(Folds  ``bag-filter  bag-null``  0  THEN  Auto)\mcdot{}

---

Home Index