coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]Is extensionality required ?

From: "Eric Jaeger" <eric.jaeger AT sgdn.pm.gouv.fr>
To: <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club]Is extensionality required ?
Date: Thu, 1 Feb 2007 21:55:48 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: SGDN / DCSSI

Hi,

Is this result provable in Coq without additional axiom ?

Theorem f_abst:forall (dom ran:Set)(P:(dom->ran)->Prop)(f:dom->ran), P f->P (fun (d:dom)=>f d).

I mean, f and (fun (d:dom)=>f d) are more than extensionnally equal... What do you think ?

Thanks for any help, Eric

Re: [Coq-Club]instantiating an inner existential, Keiko Nakata
- Re: [Coq-Club]instantiating an inner existential, Pierre Casteran
  - Re: [Coq-Club]instantiating an inner existential, Lionel Elie Mamane
    - [Coq-Club]Is extensionality required ?, Eric Jaeger
      - [Coq-Club]Re: Is extensionality required ?, Lionel Elie Mamane