Checking injectivity of receiver for a predicate with no argument crashes

[tdardinier]

When inhaling or exhaling quantified permissions with predicates, Viper checks that the arguments of the predicate is injective in the quantified variables. Both Carbon and Silicon do this with reduceLeft, which crashes when the predicate has no argument, as in the following example

predicate P()

method test()
  requires P()
  ensures forall i: Int :: i == 0 ==> P()
{}

Corresponding Carbon issue

[fpoli]

It seems this has been fixed in #597