I have the following context

```
2 goals (ID 731)
a : Node
children0 : list Node
head : Node
tail : list Node
H : head :: tail = a :: children0
============================
```

How can I prove that a = head and tail=children0?

Note that we know that a and head are the heads of their respective lists, because they are of type Node.

Node is a inductive type I have defined.

I have tried intuition and constructor, without success.

`injection H`

thanks @Gaëtan Gilbert it worked!

Roland Coeurjoly has marked this topic as resolved.

Last updated: Feb 01 2023 at 13:03 UTC