inline "cic:/CoRN/ftc/Partitions/Partition.ind".
-coercion "cic:/matita/CoRN-Decl/ftc/Partitions/Pts.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/ftc/Partitions/Pts.con 0 (* compounds *).
(*#* Two immediate consequences of this are that [ai [<=] aj] whenever
[i < j] and that [ai] is in [[a,b]] for all [i].