The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Sun, Jul 14, 2013 at 7:04 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:

> Maybe, though, your problem domain actually admits some simple proof
> automation, such that there's no need to think about case split details
> yourself.

Well, I'll certainly have a look at Chapter 14 (and perhaps earlier
chapters) to see if it fits my situation. Thanks!

In the meantime, if anyone has a direct answer to my question —like a
specific tactic that does what I need— I'd still like to know.

--
www.mhelvens.net