So let me see if I follow the definition of append there, using Fexl notation which doesn't use pattern matching (all data items such as lists are just functions applied normally).<p>Here's the fold function:<p><pre><code>  \fold = (\func\val\list list val \head\tail func head (fold func val tail))
</code></pre>
And here's the traditional definition of append, not using fold:<p><pre><code>  \append = (\xs\ys xs ys \head\tail cons head (append tail ys))
</code></pre>
The article alleges that append can be defined in terms of fold as:<p><pre><code>  \append = (\xs\ys fold cons ys xs)
</code></pre>
So now I'll try to prove the equivalence as follows.<p><pre><code>  : append xs ys

  = fold cons ys xs

  = (\func\val\list list val \head\tail func head (fold func val tail)) cons ys xs

  = \func=cons \val=ys \list=xs list val \head\tail func head (fold func val tail)

  = xs ys \head\tail cons head (fold cons ys tail)

  = xs ys \head\tail cons head (append tail ys)
</code></pre>
Looks right!