Hereditary substitution An explanation of an Agda mechanization of hereditary substitution by Keller and Altenkirch. Agda code for a PSU PL Club talk that I gave on April 19, 2013. Here are the slides for the talk.