1. T : Type
2. eq : EqDecider(T)
3. x : T
4. b : T List
5. ¬(x ∈ b)
⊢ (b|¬x) = b ∈ bag(T)
{ RepUR ``bag-co-restrict bag-filter`` 0⋅ }
⊢ filter(λz.(¬b(eq x z));b) = b ∈ bag(T)