internal

{sorts s, t

funs o, q : s -> t

. o = q;

}

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

s : Type

t : Type

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

o : s -> t %(fun)%

q : s -> t %(fun)%

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

o = q