actualize
bag-union
with
nat
by morphism
:bag → nat-bag;
:elem → nat;
∅ → ∅;
++ → ++;
count → count;
{ } → { };
-- → --;
∪ → ∪;
\ → \;
# → #;
∈ → ∈;
⊆ → ⊆;
a → n2;
b → n3;
c → n4;
bag → bag;
bag0 → bag0;
bag1 → bag1;
bag2 → bag2
end actualize