speed up some proofs

... with the aid of the -time command, available from coq's "trunk"
branch, to which we are switching.