is another definition of
list that is polymorphic over the type of
the list contents. It is a rewrite of
list type parameterized over content type. All proofs and
definitions are re-done.
For your reading enjoyment I’ve also added some basic LTac definitions
that take advantage of Coq’s proof scripting capability.
LTac is a
powerful language for writing tactics and reusing proofs. IN this
example I use it to automate induction proofs. I also use
autorewrite and rewrite databases to automate some mundane rewriting