Symm and Not_Symm Rule

We have decided a while ago already to add two new proof rules to Alethe but have not added them to the Standard yet:

https://alethe.zulipchat.com/#narrow/stream/304854-isabelle-reconstruction/topic/Not_Symm/near/259117445

SYMM corresponds to the first case in this graphic (from the cvc5 proof calculus), the NOT_SYMM to the second. They are already used in cvc5, Isabelle and Carcara.

assigned to @hjsc

closed