Add a dependent version of minus1Trunc_map
Do Exercise 7.1 from the book
Add many variants of the [simpl rewrite] tactic

It's unfortunate that Coq doesn't give us a notation of saying "this
takes anything that rewrite can take".  But these are useful for
making tactic scripts conceptually clearer.
Merge pull request #351 from JasonGross/ex-7-1

Exercise 7.1
I am merging as this is a small change which does not seem very critical.
Please let me know if this is too quick.
Merge pull request #355 from JasonGross/more-rewrite

Add many variants of the [simpl rewrite] tactic

Merging, this seems like harmless notation.