How can I prove the following free theorem with the plugin Paramcoq?
Lemma id_free (f : forall A : Type, A -> A) (X : Type) (x : X), f X x = x.
If it is not possible, then what is the purpose of this plugin?
How can I prove the following free theorem with the plugin Paramcoq?
Lemma id_free (f : forall A : Type, A -> A) (X : Type) (x : X), f X x = x.
If it is not possible, then what is the purpose of this plugin?
The plugin can generate the statement of parametricity for any type. You will still need to then declare it as an axiom or an assumption to actually use it: