Switched to a more orthogonal representation of introduction and eliminations rules for negation