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 H
into H1
?
If Grey
and None
are both constructors of an inductive type, the discriminate h
tactic will conclude the goal if h : Grey = None
.
If Grey
and None
are constructors, then they are indeed different. You can rewrite
H
into 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: Oct 13 2024 at 01:02 UTC