Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac.

Jason Gross, Andres Erbsen, Adam Chlipala

Browse the full ITP paper archive.