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)%