Mercurial > cpdt > repo
annotate src/AxiomsImpred.v @ 208:b9e9ff52913c
Port InductiveTypes
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 09 Nov 2009 11:09:50 -0500 |
parents | 7fd470d8a788 |
children |
rev | line source |
---|---|
adamc@173 | 1 (* Copyright (c) 2008, Adam Chlipala |
adamc@173 | 2 * |
adamc@173 | 3 * This work is licensed under a |
adamc@173 | 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 |
adamc@173 | 5 * Unported License. |
adamc@173 | 6 * The license text is available at: |
adamc@173 | 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ |
adamc@173 | 8 *) |
adamc@173 | 9 |
adamc@173 | 10 (* Additional axioms not in the Coq standard library, including those that need impredicativity *) |
adamc@173 | 11 |
adamc@173 | 12 Set Implicit Arguments. |
adamc@173 | 13 |
adamc@173 | 14 Require Import Axioms. |
adamc@173 | 15 Export Axioms. |
adamc@173 | 16 |
adamc@173 | 17 Theorem ext_eq_forall_Set : forall (A : Type) |
adamc@173 | 18 (f g : A -> Set), |
adamc@173 | 19 (forall x, f x = g x) |
adamc@173 | 20 -> @eq Set (forall x, f x) (forall x, g x). |
adamc@173 | 21 intros. |
adamc@173 | 22 rewrite (ext_eq _ _ _ H); trivial. |
adamc@173 | 23 Qed. |
adamc@173 | 24 |
adamc@173 | 25 Ltac ext_eq := (apply ext_eq || apply ext_eq_Set |
adamc@173 | 26 || apply ext_eq_forall || apply ext_eq_forall_Set); intro. |