The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

Hi,

In my proofs there are often introduced hypotheses like this:

    H : tl1 ++ tl2 = nil

To make progress it is necessary to perform the following steps:

    apply app_eq_nil in H ; destruct H ; subst.

This introduces equalities tl1=nil and tl2=nil and substitutes this into 
the goal and any other assumptions.

Is it possible to use a hint to encourage the crush tactic to perform 
such substitutions automatically?

Best regards,

Michael

--
Print XML with Prince!
http://www.princexml.com