The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Dear Gil,

Yes, it works! Well done!

Thanx and greetings from Croatia,

Marko Malikovic

> The following solution seems to work.
> ==========================
> Definition mynot {A} (a b:A) := a <> b.
> Lemma ...
> repeat (match goal with [H: context[?a <> ?b] |- _] => fold (mynot a
> b) in H end).match goal with [H: context [?a = ?b] |- _] => ...
> end.unfold mynot in *.
> ==========================
> Best,Gil