I managed to have both
H1: V1 & V2 == set0 and
H2: V1 & V2 != set0 in my context (with back-quoted, it's a
setI), with goal
exfalso tends to do that), but I don't get how to finish the proof. I thought I could get away with
exact H2 H2, but I get issues with
Either of these should do the trick:
by rewrite H1 in H2.
by case: eqVneq H1 H2.
BTW, if you want to insert backquotes inside backquoted markdown you only need to add a backquote to the outermost ones, as in
``H1 : V1 `&` V2 == set0``
Last updated: Jan 30 2023 at 11:03 UTC