coq-alpha-pearl This is a Coq formalization of "Functional Pearls: α-conversion is easy" (Altenkirch, 2002). Please see README.pdf for more detail.