The function push always agrees with the identity function or with setof

list(usable).
a(push,x) = x | a(push,x) = a(setof,x).
end_of_list.

Proof that the function push always agrees with the identity function or with setof | OTTER output file

up show outline