How can this goal be solved?

```
Goal forall A:Type,
[::]
\in (fun w0 : seq A => match w0 with
| [::] => true
| _ :: _ => false
end).
Proof.
```

Could we transform this to:

```
(fun w0 : seq A => match w0 with
| [::] => true
| _ :: _ => false
end) [::] = true.
```

Last updated: Jul 15 2024 at 21:02 UTC