Completed ProofObjects Chapter

This is awesome.  I think I still like Agda better for direct
construction of proof objects, but yeah.  This makes me very happy.
Programming with tactics is also pretty great.