Question: Motivation behind trigger in LemmaMaxOfConcat

[dnezam]

Looking through src/Collections/Sequences/Seq.dfy I noted the following postcondition for LemmaMaxOfConcat:

ensures forall i {:trigger i in [Max(xs + ys)]} :: i in xs + ys ==> Max(xs + ys) >= i

In particular, the trigger looks a bit unusual. I would have expected it to be something along the lines {:trigger i in xs + ys}. Is there a specific reason as to why it is the way it is?

I hope this kind of question is fine to ask here as an issue.