Polymorphic minimal propositional logic

Redo that exercise , proving universally quantified closed statements instead of using some predeclared propositional variables.
For instance, instead of declaring P:Prop and proving the proposition P->P, prove the proposition forall P:Prop, P->P.
You may do this exercice by removing every call to auto from this file