eliminators-0.3: Dependently typed elimination functions using singletons

This library provides eliminators for inductive data types, leveraging the power of the singletons library to allow dependently typed elimination.