Mercurial > cpdt > repo

annotate src/AxiomsImpred.v @ 245:4b001a611e79

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prose for old part of Firstorder
author Adam Chlipala <adamc@hcoop.net>
date Wed, 09 Dec 2009 15:26:22 -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.