Author: Conor McBride
Title: Standard Equipment for Inductive Datatypes
Abstract: 
Every inductive datatype can be equipped with useful (if unremarkable)
theorems by following some standard 'recipes': constructors are injective
and disjoint; constructor-guarded recursion is admissible; cyclic
equations are false. Given a heterogeneous equality, these recipes
extend straightforwardly to indexed families of datatypes (in a way that 'equality-respects-predecessor' proofs of injectivity do not, for
example). This technology is five years old, so it is time that I
explained it properly.