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