eliminators

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