Applications written in Coq-Elpi Derive Given an inductive type declaration it synthesizes a bunch of useful stuff such as proved equality tests, projections, parametricity relations. Eltac A toy set of tactics implemented in Elpi. NES A Namespace Emulation System.