[auto-reverse] apply reversible selection

[olaure01]

Fixes #64

[etiennecallies]

There is an infinite loop :( Because this is a recursive function.

Ex: ?A -> A,?A -> A,A,?A -> A,A,A,?A -> ... -> A,...,A,?A

It's very different spirit form previous auto-reverse rules :

• the other rules only apply one rule
• the other rules simplify the sequent, whether this one makes it longer.

Perhaps we should rethink it.

[olaure01]

Absolutely!
It is meaningless to apply twice the reversible selection rule in a given asynchronous phase.
I will correct it.

[etiennecallies]

See video on #64 : we should prevent selection if it has been already applied.

[olaure01]

Selection is not applied anymore if sub-formula already present.
I see 3 possible directions:

• do not use reversible selection at all
• use it as done here: iterated action of the user on the auto-reverse button could repeat applying selection, but it is not so unnatural since it is on request of the user
• [my favorite] add a sub-option to auto-reverse mode for incorporating selection or not (can rely on auto_reverse_selection Boolean in auto_reverse_sequent.ml)