I decided to simply Print the original definition instead of working around redefinition.
I think that working around redefinition would be a wrong choice, because a reader wouldn't be able to use lemmas proved for the original definition in the exercises.
I didn't update /docs/pnp.pdf with this commit because I wanted to avoid binary noise in case changes are necessary. You can see updated book here: http://srv04.mikr.us:30449/tmp/pnp.pdf
This pull request aims to resolve #18 .
I decided to simply
Printthe original definition instead of working around redefinition. I think that working around redefinition would be a wrong choice, because a reader wouldn't be able to use lemmas proved for the original definition in the exercises.I didn't update
/docs/pnp.pdfwith this commit because I wanted to avoid binary noise in case changes are necessary. You can see updated book here: http://srv04.mikr.us:30449/tmp/pnp.pdf