Do exercise 6.9, add some minor lemmas about pointed types

The pointed types lemmas are in preparation for some other 6 exercises.