Yeah, that's there. We need both operators to be strict, I think; otherwise we can't really assume anything about what they'd return for NULL inputs. But if they are, we have NULL => NULL which is valid for all proof cases.
I understand. I don’t see any problems in this case.
