`eq_symmetric` rule

As part of elaborating a proof in Carcara, we attempt to completely remove the implicit reordering of equalities, and to do so we need rules that reason about the symmetry of equality. The recently added symm and not_symm rules help in many cases, but it would also be useful to have a rule that concludes the tautology (= (= a b) (= b a)). While in theory we could derive this conclusion using the existing symm rule, it would be very cumbersome to do so, requiring several steps including a subproof. Instead, I propose the addition of a new rule, eq_symmetric, that takes no premises and concludes a single term of the form (= (= a b) (= b a)):

(step t1 (cl (= (= a b) (= b a))) :rule eq_symmetric)

While it's not ideal that this rule has such a similar purpose to an already existing one, there are already a few other similar cases in Alethe (trans/ eq_transitive, equiv1/equiv_pos2, etc.).