Fixing injectivity checks for QPs with multiple quantified variables

[marcoeilers]

This fixes #378. The injectivity check is not actually missing, but it's incorrect (also for fields).

For a QP of the form forall x, y :: cond ==> P(e1, e2), the current code essentially generated the following injectivity check:

assert forall x, x', y, y' :: (x != x' && y != y') && cond && cond' ==> (e1 != e1' || e2 != e2')

This is incorrect. We need to check that if the value of any quantified variable changes, we get a different tuple of receiver expressions, but we're checking that if the values of all quantified variables change, we get a different tuple. Essentially, we need to check that the receiver tuple is injective in all quantified variables, but the current check also succeeds if it's injective only in one of them.

So this PR changes the check to

assert forall x, x', y, y' :: (x != x' || y != y') && cond && cond' ==> (e1 != e1' || e2 != e2')

[viper-admin]

LGTM!