sort s;

op f : s --> s;

. f = ((\ x : s . x) as s --> s)

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

s : Type

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

f : s --> s %(op)%

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

f = ((\ x : s . x) as s --> s)