I usually try to turn my `case: T`

into `have [] := T`

but this does not work here I don't why.

This works

```
Goal forall x1 x2 : nat,
match x1 =P x2 with ReflectT _ => True | ReflectF _ => False end.
move=> x1 x2.
case: (x1 =P x2).
```

This does not work

```
Goal forall x1 x2 : nat,
match x1 =P x2 with ReflectT _ => True | ReflectF _ => False end.
move=> x1 x2.
have [] := x1 =P x2.
```

what am I missing?

I'd expect the first one destructs the occurrence of your T in the context, while have isn't supposed to do that...

Last updated: Jan 29 2023 at 19:02 UTC