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