add singleton_mono
This just came up in a proof in Perennial. I am not sure about the best name for the lemma though; "mono" does not say wrt. which relation it is monotone.
This just came up in a proof in Perennial. I am not sure about the best name for the lemma though; "mono" does not say wrt. which relation it is monotone.