Library Coq.funind.FunInd


Require Coq.extraction.Extraction.