The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Wed, Dec 23, 2015 at 12:19:53AM +0100, Robbert Krebbers wrote:
> >     rewrite foo; last by eauto using foo bar baz.
> >
> This is problematic when rewriting with foo gives rise to multiple
> side-conditions. Does ssreflect have a construct similar to "first"/"last"
> that applies a tactic to all generated subgoals _apart from_ the first/last
> one?

I'm afraid there is no such construct in ssreflect.

The only thing I can suggest is to "tune" the statement of the lemma.
I mean, if foo is supposed to always generate 3 subgoals, all solvable by
a tactic like eauto, then rephrasing is as "c1 /\ c2 /\ c3 -> a=b" may
be worth it.

Hope it helps,
-- 
Enrico Tassi