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: Jan 31 2023 at 14:03 UTC