Stream: Coq users

Topic: ✔ Prove heads of equal lists are equal

Roland Coeurjoly Lechuga (Jun 08 2022 at 19:48):

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.

Gaëtan Gilbert (Jun 08 2022 at 19:50):

injection H

Roland Coeurjoly Lechuga (Jun 08 2022 at 19:59):

thanks @Gaëtan Gilbert it worked!

Notification Bot (Jun 08 2022 at 19:59):

Roland Coeurjoly has marked this topic as resolved.

Last updated: Sep 23 2023 at 15:01 UTC