Add lemmas for big_opS and gmap singletons

This is a particular pattern that comes up in the lifetime logic which I want to be able to rewrite, which is why I've extracted it to a general lemma.