The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

Hi Tillmann,

On Sun, Apr 19, 2009 at 03:55:48PM +0200, Tillmann Rendel wrote:
> 
> However, it is even easier to instantiate the WDecide functor from 
> library FSetDecide for your particular FSet, and use the tactic fsetdec.

Thanks, this is great!

In my real proof this sits there thinking for long enough for me to get
bored and kill it, but if I do a
    clear - oa_eq_add_o_a oab_eq_add_a_add_b_o.
first then it goes through.


Thanks
Ian