Given a list, while doing case analysis in proof mode, is there a way

to split like `[], [a], a::l'`

instead of the usual `[], a::l'`

?

For a scenario like this:

```
Require Import List ssreflect.
Import ListNotations.
Goal forall (A:Type) (l : list A),
match l with
| [] => 0
| [a] => 1
| _ => 2
end = length l.
Proof.
move => A l.
case l.
- by [].
- move => a2 w2.
case w2.
+ by [].
+ move => a3 w3.
by [].
```

`move=> A [| a [| l']]`

Thanks!

Julin Shaji has marked this topic as resolved.

In vanilla Coq, `intros A [|a [|l']].`

does the same

Last updated: Jun 23 2024 at 03:02 UTC