Adding cut elimination example and the current state of the abella proof.