modified efxmap`leq-implies-permission-leq and
efxmap`leq-implies-permission-leq-converse to take
only one cxt-efxmap relation in premise - the other
can be inferred using this information and efxmap`leq.