The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Andreas Lundblad wrote:
> I've run into a situation, similar to the situation below. 
[...]
> Theorem test :
>   forall l,
>     nth 2 l 7 = 0 ->
>     0 = ((fix func (l0: list nat) :=
>       match nth 2 l0 7 with
>         | 0 => 0
>         | _ => 1
>       end) l)

I don't think this example quite expresses the important issues here, 
because your [fix] isn't recursive.  You could rewrite it as a simple 
[fun] and then probably prove the theorem without trouble.

Generally, a [fix] application only reduces when the top-level 
constructor of the recursive argument is known.  For your example, you 
can [destruct l] to reduce the theorem to two simple cases.