> 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.
