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

s : Type

t : Type

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

snd : s � t -> t = \ (x : _var_35, y : _var_45) . (op y : _var_45)

%% Diagnostics -----------------------------------------------------------

Error (line 5, column 9) different terms of 'snd'

\ (x : _var_35, y : _var_45) . (op y : _var_45)

\ (x : s : s, y : t : t) . (op y : t)

Error (line 6, column 9) different terms of 'snd'

\ (x : _var_35, y : _var_45) . (op y : _var_45)

\ (x : s : s, y : t : t) . (op y : t)