internal

{sort s, t;;

fun o, q : s -> t;;

. o = q;

}

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

s : Type

t : Type

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

o : s -> t %(fun)%

q : s -> t %(fun)%

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

o = q