work on new length_snoc. contradiction in hypotheses?