sort t;

op f : ? t -> t;

op g : t -> (? t);

op a, b : t;

op c, d : ? t;

. f a = g c

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

t : Type

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

a : t %(op)%

b : t %(op)%

c : ? t %(op)%

d : ? t %(op)%

f : ? t -> t %(op)%

g : t -> ? t %(op)%

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

f a = g c