for n, m being Nat
for X being ConstructorDB
for A being FinSequence of the Constrs of X st n <= m holds
ATLEAST- (A,n) c= ATLEAST- (A,m)