Recover concrete multiset reasoning by making it possible to trigger multiset properties based on push

[utaal]

@Chris-Hawblitzel: e.g. by having the seq! macro produce an auxiliary term that, through an optional broadcast, would allow to trigger the multiset ensures

cc @ahuoguo @LailaElbeheiry