finished last 2 coq proofs in chap01