Hi, I currently struggle with the following proof obligation.
x : Node H : mV x = Grey H1 : mV x = None ============================ sndi x
From my (limited) understanding, this is already a contradiction since both
H : mV x = Grey and
H1 : mV x = None can't be true. Any help is highly appreciated.
Hi. Have you tried rewriting
None are both constructors of an inductive type, the
discriminate h tactic will conclude the goal if
h : Grey = None.
None are constructors, then they are indeed different. You can
H1 and then
discriminate over the new equality.
There is also the
discriminate variant which finds the equality on its own.
Thank you both, this was the missing part, which tool me hrs :P Zulip chat is such a help getting started.
Last updated: Jan 31 2023 at 14:03 UTC