The Coq mailing list

[Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>]

Hi,

I have the following simple goal which is not solved by “eauto.” but is solved by "destruct H1 as [w1 [R1 H1]]. eauto.”  . Is there any other “auto-like” tactic that would try “destruct” automatically for me?

w : i

p : o

q : o

H1 : exists w1 : i, r w w1 /\ p w1

H2 : forall w1 : i, r w w1 -> p w1 -> q w1

______________________________________(1/1)

exists w1 : i, r w w1 /\ q w1

Best regards,

Bruno