Add utils to follow the path to an incorrect proof step and to create an error message from invalid proof judgement