Walkthrough of beq_symb_ok tactic

This coq script steps through the beq_symb_ok tactic from color VSignature as an example of how to do a beq_symb_ok proof, and how handy tactics and the semi-color operator are for automating tedious case analysis.