[ new ] From ILL to Tactics for Bag equivalence

This is based on Nils Anders Danielsson's definition of Bag equivalence.
http://www.cse.chalmers.se/~nad/publications/danielsson-bag-equivalence.html

I claimed that the theory with tensors only was the one of Bag equivalence
so we might as well formalise this given that it does not take an awful
lot of work. And nad's library is quite nice to study / use.