(* equality is handled in a special way: in particular,
the type, if defined, is always added to the prefix,
and n is not decremented - it should have been n-2 *)
(* equality is handled in a special way: in particular,
the type, if defined, is always added to the prefix,
and n is not decremented - it should have been n-2 *)