Hi,

I have a lemma : `Lemma subsetNeqSetDnonempty {T} (X Y : set T) (H : X `<=` Y) : X != Y <-> (Y `\` X) != set0.`

that I managed to prove. I'd like to convert it to an equality instead of an equivalence: `Lemma subsetNeqSetDnonemptybis {T} (X Y : set T) (H : X `<=` Y) : (X != Y) = ((Y `\` X) != set0).`

. However when I try to do rewrite propeqE at the very beginning, I get an error ```
The LHS of propeqE
(_ = _)
does not match any subterm of the goal
```

. Is it because I have an hypothesis H ? I noticed that it works if I change the goal to `((X `<=`Y) /\ X!=Y) = ((Y `\` X) != set0)`

but I don't understand why.

Last updated: Jun 25 2024 at 18:02 UTC