while (cit!=last) {
const ex & expanded_ex=(*cit).rest.expand(options);
if (!are_ex_trivially_equal((*cit).rest,expanded_ex)) {
while (cit!=last) {
const ex & expanded_ex=(*cit).rest.expand(options);
if (!are_ex_trivially_equal((*cit).rest,expanded_ex)) {