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: Oct 13 2024 at 01:02 UTC