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 False
(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 is_true
...
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``
@Cyril Cohen excellent, thanks!
Julien Puydt has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC