  We introduce the notion of identity coercions between non-indexed and indexed
variants of inductive datatypes, such as lists and vectors. An identity
coercion translates one type to another such that the coercion function
definitionally reduces to the identity function. This allows us to reuse vector
programs to derive list programs (and vice versa), without any runtime cost.
This also allows us to reuse vector proofs to derive list proofs (and vice
versa), without the cost of equational reasoning proof obligations. Our work is
formalized in Cedille, a dependently typed programming language based on a
type-annotated Curry-style type the- ory with implicit (or, erased) products
(or, dependent functions), and relies crucially on erasure to introduce
definitional equalities between underlying untyped terms.
