Iteration and (partly) subscript access not handled generically

[marcoeilers]

Currently, we handle iteration (and therefore quantification) over a collection as well as, to a lesser degree, subscript access, by special casing Nagini for the classes for which this is relevant (e.g., the resolver has special cases for this for defaultdict and expiringdict, when it really shouldn't). There should be a more generic way to solve this problem.