I also renamed `iProof` into `iStartProof`, as it is supposed to be
something internal, and not a substitute of Coq's `Proof` command (as
originally intended).