feat: variant for up-to-bad call/proc tactics

[loutr]

The premise:

∀O. is_lossless O => is_lossless A(O)         (1)

of the current up-to-bad tactics happens to be too restrictive in some cases. At first glance, it seems that it would be possible to allow another variant of the tactic that instead requires

is_lossless A(O_1) ∧ is_lossless A(O_2)       (2)

(possibly as two differents subgoals), which can be proved in some concrete instances of A, O_1, O_2, while (1) is not.

Simply introducing a variant of the tactic that replaces (1) with (2) is not satisfactory and is not ensured to be sound.

This is because commit 6534f3d (yes, some archeology was required) changed the premises of this tactic, which implicitly changes the proof of soundness of the tactic.

In order to have a sound variant of the tactic, this PR provides a way to use a different set of premises, which restores the original conditions required for applying up-to-bad tactics, as well as changes condition (1) with (2) (which is the original goal).

Some issues still need to be addressed w.r.t. parsing. Introducing a variant syntax in the spirit of call @[weaker_pre] causes shift/reduce conflicts.

---

This is a duplicate of PR #1055 that was incorrectly targeting the main branch of my fork. This is an error on my side.

[strub]

@loutr

This is a duplicate of PR #1055 that was incorrectly targeting the main branch of my fork. This is an error on my side.

You can always change the target branch (when editing the title, the target branch can be changed)

[strub]

In order to have a sound variant of the tactic

I thought that the previous tactic was still sound. If not, this is not a variant that should be introduced. We should get rid of the previous one.