Make 'that is equivalent to' a standalone tactic

Simplify AST types, parsing rules and pp of tactics that had
'that is equivalent to' or 'or equivalently'

Modify grafiteEngine accordingly

Simplify the signature and the code of the implementations of tactics
that had 'that is equivalent to' or 'or equivalently'

A new "volatile_hypo" key is added to the parameter list of the currest
stack level to indicate that the beta rewriting should happen on that
hypothesis, instead of the thesis

Modify beta_rewrite accordingly

Add some "obvious" terms to the given candidates for the automation
(such as refl, sym_eq, trans_eq, etc.)

The weakening of the automation is now only partial: the second flag for
weakening is off. Setting it on makes theorem proving pretty impossible
with the declarative fragment.