dcon append : term -> term -> term -> type.

%mode append +D +D -D.

append nil Y Y.

append (cons X N) (cons X M) : append N M M.

%worlds (term term term) (append).

%total D (append).