This patch improves shrinking behavior for values from "text()" and
"binary()" which contain duplicate elements, like ""zzzabc"". It also
improves shrinking for bugs which require the same character to be
drawn from two different "text()" strategies to trigger.
The canonical version of these notes (with links) is on readthedocs.