push is one-to-one

list(usable).
a(push,x1) != a(push,x2) | x1 = x2.     %    (not used in later proofs)
end_of_list.

Proof that push is one-to-one | OTTER output file

up show outline