We develop a library for finite sets using Ssreflect. In contrast to the "finset" library in Ssreflect, which only allows finite base types, we allow countable types as base types. Finite sets are implemented as a quotient on lists using some canonical duplicate free list as representative. We provide most of the basic theory as well as constructions for least and greatest fixpoints and maximal extensions.
Theory Files (requires mathcomp-ssreflect-1.6)
Theory Files (requires ssreflect-1.5)
Completeness and Decidability Results for CTL in Coq (ITP 2014)
Completeness and Decidability Results for CTL in Coq (Extended Version)