Add some theorems about oevery and oexists

Define the concept of a function respecting the equivalence that arises
from the comparison operator. oevery and oexists should only be used
with such functions.