hmm, I'd have thought the second snake equation should be an independent fact in its own right rather than merely the result of applying op to the first.

I think it should look like this (apologies for the hand drawn picture!):

![second-snake](https://i.imgur.com/sydXrFJ.jpg)