Grammar nit: "Coq will automatically [find|infer] a proof".  Also, I think "For" should be "for" and "Unit" should be "[Unit]"