Skip to content

add singleton_mono

Ralf Jung requested to merge ralf/singleton_mono into master

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.

Merge request reports