Fixed bugs in showproofs, and stopped backward-infer from returning to the node it just came from.