I have a function with two arguments f(a b) , while f checks the equality of a and b.First time it consider it true next false.But i want to make it visible in hypothesis like H:a=b next a<>b .(I have applied destruct as H ,but get this message "Disjunctive/conjunctive introduction pattern expected."

In the following context:

```
Variables (A: Type)(f : forall a b:A, {a = b}+{a <> b}).
```

You may try `destruct (f a b) as [Heq | Hneq].`

Last updated: Jun 24 2024 at 13:02 UTC