Short cut fusion is a particular technique which uses a single,
local transformation rule --- called the foldr-build rule ---
to remove certain intermediate data structures from modularly
constructed functional programs. Arguments that short cut fusion is
correct typically appeal either to intuition or to ``free theorems" ---
even though the latter have not been known to hold for the Haskell-like
languages in which it is usually applied. In this paper we use Pitts'
recent demonstration that observational equivalence in such languages
is relationally parametric to provide the first formal proof that
programs which have undergone short cut fusion are observationally
equivalent to their unfused counterparts. The same techniques in fact
yield a much more general result: For each algebraic data type we can
define a generalization of build which constructs substitution
instances of algebraic data structures, and prove correct an
observational equivalence-preserving cata-augment fusion rule
which optimizes compositions of functions that uniformly consume
algebraic data structures with functions that uniformly produce
substitution instances of them.
