The Coq mailing list

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

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