coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] inversion vs injection

From: t x <txrev319 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] inversion vs injection
Date: Tue, 3 Sep 2013 18:45:51 +0000

Hi,

Can someone povide a minimal example of a case where "injection" make progress where "destruct/induction/inversion" can not?

"injection" is clearly important since there is a tactical named after it; but it seems like every time I want to break something, destruct/induction/inversion does it.

It's not clear to me when I should use injection.

Thanks!

[Coq-Club] inversion vs injection, t x, 09/03/2013