eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
fully authentic merge;
(benchmark Isabelle
:extrafuns (
(uf_1 Int)
(uf_2 Int)
(uf_3 Int)
)
:assumption (not (= (+ uf_1 (+ uf_2 uf_3)) (+ uf_2 (+ uf_3 uf_1))))
:formula true
)