The Coq mailing list

["Edward Z. Yang" <ezyang AT mit.edu>]

I recently found myself writing the following tactic:

(**)
Ltac exbamf := match goal with
                 | [ H : _ -> exists _, _ |- exists _, _ ] => destruct H
                 | [ H : forall _, _ -> exists _, _ |- exists _, _ ] => 
edestruct H
                 | [ H : forall _ _, _ -> exists _, _ |- exists _, _ ] => 
edestruct H
                 | [ H : forall _ _ _, _ -> exists _, _ |- exists _, _ ] => 
edestruct H
               end.
(**)

Is there a way to write this more cleanly?

Edward