The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On Sun, 27 Nov 2011 03:00:43 +0100, 
alexander AT math.ohio-state.edu
 wrote:
> For a full compilable file to put the below examples in context, see
> http://www.math.osu.edu/~alexander/variadic/variadic4.txt

This seems to be giving me a redirection loop.

>    Synterp_func (existT (fun _ : Term => Assignment) (apply f u v) s) =
>    M1 f (Synterp_func (existT (fun _ : Term => Assignment) u s))
>      (Synterp_func (existT (fun _ : Term => Assignment) v s))
> 
> What the?!  I can't make sense of this.  I cannot complete the proof of the
> lemma, which ought to be as simple as "auto." since it's taken directly from
> the definition of Synterp.

Have you tried unfolding Synterp_func?
Syninterp_func takes all the arguments as dependent tuple, and Syninterp
is a wrapper around it, so you can pass the arguments you expect.

  Tom