+ integral indexes).
+
+ Luckily enough, in practice types dependent overs setoids occur very rarely.
+ Most examples of dependent types are indexed over discrete objects, like
+ natural, integers and rationals, that admit an unique representation.
+ For continuity reasons, types dependent over real numbers can also be
+ represented as types dependent over a dense subset of the reals, like the
+ rational numbers. *)