internal

{type s, t;

fun o, q : s -> t;

. (fun o : s -> t) = (fun q : s -> t)

}

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

s : Type

t : Type

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

o : s -> t %(fun)%

q : s -> t %(fun)%

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

o = q