The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi,

On Fri, May 10, 2013 at 10:23:26AM +0200, Dimitur Krustev wrote:
> 'rewrite' works best for me in cases like this, but there are also the
> 'apply ->' and 'apply <-' variants of 'apply', specifically aimed at
> working with 'iff'.
> 
> In the example, 'apply -> Qlt_alt; auto' is enough to finish the proof.

Wow! I was sure 'apply ->' and 'apply <-' were not syntactically correct.
I thought I had tested them (since they are the first obvious idea)...

But indeed, you are right, they work. Thanks.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/