The Coq mailing list

[Zoe Paraskevopoulou <zoe.paraskevopoulou AT gmail.com>]

I see, it gets quite technical indeed. 

> On Mar 30, 2015, at 5:32 PM, Matthieu Sozeau 
> <mattam AT mattam.org>
>  wrote:
> 
> Aha, it's non-trivial indeed but you can do the unfolding trick. Maybe
> you didn't get the right induction hypothesis because you need to redo
> the well-founded induction in the lemma, and also generalize by the ie
> variable.

I fact my naive approach didn't get me that far, I was stuck when I was 
trying to prove extensional equivalence with the unfolded definition, so I 
never got into the final lemma where well founded induction is required to 
handle the abstraction case. 

Thanks again,
Zoe