package coq-paramcoq

A Coq plugin providing commands for generating parametricity statements. Typical applications of such statements are in data refinement proofs. Note that the plugin is still in an experimental state - it is not very user friendly (lack of good error messages) and still contains bugs. But it is usable enough to "translate" a large chunk of the standard library.