for l being quasi-loci
for s being SortSymbol of MaxConstrSign
for m being constructor OperSymbol of s st len (the_arity_of m) = len l holds
variables_in (m -trm (args l)) = rng l