Don't always "drill to the bottom" and unfold to sums; instead
explicitly make use of the fact that the EDF proof reasons about
finite identical prefixes, which allows staying at a semantically
higher level in the proof.

While at it, switch the file to using the preferred `now` tactical
when closing out proofs (rather than `by`) to avoid emacs indentation
issues.