The Coq mailing list

[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