for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y holds ATMOST+ (B,0) = ATMOST B