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