Quantified permissions for list entries based on indices result in errors

[marcoeilers]

When specifying permissions to the elements of a list based on their indices, e.g. as follows:

Forall(range(0, len(l)), lambda i: Acc(l[i].value))

Viper raises an error complaining that the receiver of the quantified permission is not injective (and Nagini currently crashes when trying to translate the error message).
While it is possible to specify permissions like these based on list containment, i.e.

Forall(l, lambda e: Acc(e.value))

Nagini then doesn't always realize that this gives the permission required for referencing l[i].value elsewhere.