The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Fri, Jul 19, 2013 at 9:46 PM, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:

>> If possible, I'd still like a response to my question (1).
>
> This is something like what I'd expect a mutual induction principle to
> look like:

That looks like it took some effort. :-)

I assure you it's not wasted, because I'll study it. But my primary
question is more basic:

How can those definitions be used to get Coq to accept the definitions
of `short_lists1` and `short_lists2`?

--
www.mhelvens.net