coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Equality of functions

From: Pablo Argon <pargon AT cadence.com>
To: coq-club <coq-club AT pauillac.inria.fr>
Subject: Equality of functions
Date: Mon, 15 May 2000 19:13:38 -0700
Organization: Cadence Berkeley Laboratories

Hi all,
I wonder how to prove this simple equality :

Theorem ff_is_gg : (A,B:Set;ff,gg:A->B)
((x:A)(ff x)=(gg x))<->([x:A](ff x))=([x:A](gg x)).

Thank you in advance, Pablo

Equality of functions, Pablo Argon
- Re: Equality of functions, Eduardo Gimenez
  - Re: Equality of functions, Pablo Argon
    - Re: Equality of functions, Benjamin Werner