type s

op f : s --> s

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

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

s : Type

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

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

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

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