Mercurial > cpdt > repo

comparison src/AxiomsImpred.v @ 173:7fd470d8a788

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
System F
author Adam Chlipala <adamc@hcoop.net>
date Sun, 09 Nov 2008 15:15:41 -0500
parents
children
comparison
equal deleted inserted replaced
172:653c03f6061e 173:7fd470d8a788
1 (* Copyright (c) 2008, Adam Chlipala
2 *
3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License.
6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *)
9
10 (* Additional axioms not in the Coq standard library, including those that need impredicativity *)
11
12 Set Implicit Arguments.
13
14 Require Import Axioms.
15 Export Axioms.
16
17 Theorem ext_eq_forall_Set : forall (A : Type)
18 (f g : A -> Set),
19 (forall x, f x = g x)
20 -> @eq Set (forall x, f x) (forall x, g x).
21 intros.
22 rewrite (ext_eq _ _ _ H); trivial.
23 Qed.
24
25 Ltac ext_eq := (apply ext_eq || apply ext_eq_Set
26 || apply ext_eq_forall || apply ext_eq_forall_Set); intro.