Fixing Section 2.9, closing #446.

We say "...given...p as before", and it was correctly annotated in the previous occurrence. Thus my fix was to simply remove the part where we repeated the assumption of p (with the wrong type!). closes #446