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.
thanks @Gaëtan Gilbert it worked!
Roland Coeurjoly has marked this topic as resolved.
Last updated: Feb 01 2023 at 13:03 UTC