Coq: How to use one tactic to appoint instances for multiple existential quantified variables

Question

Suppose I have a goal as follow.

exists s0 s3 s4 : list T, s1 ++ s2 = s0 ++ s3 ++ s4 

I want to appoint some concrete values for s0, s3, s4 and I am trying exists v1 v2 v3 to do that with v1 v2 v3 already in the proof context. But coq complains that

Not the right number of missing arguments (expected 1)

So I have to use three tactics to do this.

exists v1. exists v2. exists v3.

I want to known if it's possible to use just one tactic to get the same result. Many thanks!.

Answer 1

The syntax is exists v1, v2, v3. I just tested with coq-8.13.2