5  Explaining and Checking Proofs: h1trace, h1logstrip