The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Thank you Jason. Using Definition instead of Fixpoint worked. I don't
understand the problem, though. Can anyone explain me what's wrong
with using Fixpoint here?

---
Ömer Sinan Ağacan
http://osa1.net


2014-02-13 1:12 GMT+02:00 Jason Gross 
<jasongross9 AT gmail.com>:
> Use [Definition] for [closed] rather than [Fixpoint].  Alternatively, use
> [destruct n'; simpl in *].
>
> -Jason
>
>
> On Wed, Feb 12, 2014 at 4:46 PM, Ömer Sinan Ağacan 
> <omeragacan AT gmail.com>
> wrote:
>>
>> Hi all,
>>
>> I'm stuck with this:
>>
>>
>> H3 : (fix closed (n : nat) (t : tm) {struct n} : Prop :=
>>         fvs n t = empty_set id) n' e'
>> ==========================================
>> fvs n' e' = empty_set id
>>
>>
>> Any ideas how to prove this?
>>
>> Thanks ..
>>
>> ---
>> Ömer Sinan Ağacan
>> http://osa1.net
>
>