It seems to help Dafny with instantiation of quantifiers during proofs if you give the quantified expression a name by encapsulating it in a predicate. If you don’t you can end up in a situation where you prove some quantified property, but are then unable to subsequently assert that quantified property, I think due to Dafny not understanding that the quantification is the same. Naming the property (or more likely, only writing it in one place rather than two places) fixes this.

For example rather than writing:

   ...
   ensures forall c :: P(a, c) == P(b, c);
   ...
   assert forall c :: P(a, c) == P(b, c);

Write this:

   predicate Q(a:S,b:S)
   { forall c :: P(a, c) == P(b, c) }
   ...
   ensures Q(a, b);
   ...
   assert Q(a, b);