Imaps trigger selection

[yizhou7]

The manually entered trigger seems nice here (since it may prevent the client from asserting m[i] in m). In fact, I think this may be a good candidate to generate automatically. In other words, whenever i in m is an automatic trigger, then automatically add m[i] as well. (If you agree, please this as is for now and file an Issue against dafny-lang/dafny, referring back to this line here.)

Originally posted by @RustanLeino in dafny-lang/libraries#25 (comment)