make lemma-sequenceV-successful more precise