(define f1::(-> int int))
(define f2::(-> int int))
(define i1::int)
(define i2::int)
(define v1::int)
(define v2::int)

(assert (= f2 (update f1 (i1) v1)))
(assert (= (f2 i1) v2))
(assert (/= v1 v2))