type a;

op f : a -> a

program f (v@_:a) = v