Consider making BAG_IN an overload

[mn200]

BAG_IN is redundant in the same way that MEM is; we end up proving two sets of theorems: one for BAG_IN and one for SET_OF_BAG.

To be explicit, the overload would be

overload_on("BAG_IN", ``λe b. e IN SET_OF_BAG b``)

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.