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...

ok my bad, thanks

Laurent Théry has marked this topic as resolved.

Last updated: Jul 25 2024 at 17:02 UTC