type a

op f : a -> a

program f (v @ (var _ : _v1_) : a) = v;

%% Type Constructors -----------------------------------------------------

a : Type

%% Assumptions -----------------------------------------------------------

f : a -> a %(op)%

%% Sentences -------------------------------------------------------------

program f (v @ _ : a) : a = v %(pe_f)%

%% Diagnostics -----------------------------------------------------------

### Hint 5.9, repeated declaration of 'f'