[tactic] Single sided match should work for arbitrary pre-conditions

[Cameron-Low]

Apparently trivialstruggles to deal with P /\ Q /\ R => P /\ R when either P or R are sufficiently complex (e.g. contains an existential).
This should close #775.

[alleystoughton]

Works for my example.

[namasikanam]

It also works for my minimal working example. Furthermore, it works for my original complicated example, too! Thank you so much!

[namasikanam]

I'm trying to understand what's going on in this PR. Why are you talking about trivial @Cameron-Low ? I'm completely lost.

[Cameron-Low]

I'm trying to understand what's going on in this PR. Why are you talking about trivial @Cameron-Low ? I'm completely lost.

see #EasyCrypt: questions & features > match: cannot clear c that is/are used in the conclusion @ 💬l

[strub]

@Cameron-Low Is trivial still called by the tactic? I cannot see where it is replaced by your ad-hoc tactic in the code.

[Cameron-Low]

@Cameron-Low Is trivial still called by the tactic? I cannot see where it is replaced by your ad-hoc tactic in the code.

Sorry, I had pushed the wrong version of the fix... It's all there now.

[fdupress]

Looks good to me. Made a comment phrased as a question, but it can be safely addressed by dismissal if that is the most appropriate way of addressing it.