The main development is
here
. It requires
Substitution
,
InductiveFiniteSets
,
FiniteTypes
,
FinSummDefs
and
Containers.