Exercises 3.4 and 3.5

If there is a shorter solution to 3.4, then I'd like to know (and will add/substitute).

> It's poor style to use Coq-generated names; they're somewhat  
> fragile, and confusing to the reader who isn't replaying it in Coq.   
> You should `pose (...) as p`, or `pose (p := ...)`.
>
Let me fix this, with p := equal_constant_functions (we are not afraid  
of long names?).

Marc