coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] map_eq_nil lemma

From: Taral <taralx AT gmail.com>
To: Michael Day <mikeday AT yeslogic.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] map_eq_nil lemma
Date: Wed, 7 Apr 2010 22:07:33 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=I3Kl8NZWfA54XkhTS0HhAhm6ATa9EIs+a/yQ6VimqWQhY4o+hSpZkXQeeY9j12L27Y mpPRjEvUPZIpV5V6thF70pA7i6lYm1BSq/lMbEfDzt0aJDYlwRYcjyGSXgL/i3dphqZy M1t3vrfV/5lJRxlaO/cSMKuz2Z5UOEV7RVgJc=

On Wed, Apr 7, 2010 at 9:08 PM, Michael Day
<mikeday AT yeslogic.com>
wrote:
> map_eq_nil : forall l, map f l = nil -> l = nil.

dependent destruction l; auto. ?

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
-- Unknown

[Coq-Club] map_eq_nil lemma, Michael Day
- Re: [Coq-Club] map_eq_nil lemma, Taral
  - Re: [Coq-Club] map_eq_nil lemma, Pierre Casteran
    - Re: [Coq-Club] map_eq_nil lemma, Michael Day