signature { automatic } theory
{
<>([]!N0 ^ B false)
}