adamc@173: (* Copyright (c) 2008, Adam Chlipala adamc@173: * adamc@173: * This work is licensed under a adamc@173: * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 adamc@173: * Unported License. adamc@173: * The license text is available at: adamc@173: * http://creativecommons.org/licenses/by-nc-nd/3.0/ adamc@173: *) adamc@173: adamc@173: (* Additional axioms not in the Coq standard library, including those that need impredicativity *) adamc@173: adamc@173: Set Implicit Arguments. adamc@173: adamc@173: Require Import Axioms. adamc@173: Export Axioms. adamc@173: adamc@173: Theorem ext_eq_forall_Set : forall (A : Type) adamc@173: (f g : A -> Set), adamc@173: (forall x, f x = g x) adamc@173: -> @eq Set (forall x, f x) (forall x, g x). adamc@173: intros. adamc@173: rewrite (ext_eq _ _ _ H); trivial. adamc@173: Qed. adamc@173: adamc@173: Ltac ext_eq := (apply ext_eq || apply ext_eq_Set adamc@173: || apply ext_eq_forall || apply ext_eq_forall_Set); intro.