adamc@125: (* Copyright (c) 2008, Adam Chlipala adamc@125: * adamc@125: * This work is licensed under a adamc@125: * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 adamc@125: * Unported License. adamc@125: * The license text is available at: adamc@125: * http://creativecommons.org/licenses/by-nc-nd/3.0/ adamc@125: *) adamc@125: adamc@125: (* Additional axioms not in the Coq standard library *) adamc@125: adamc@173: Set Implicit Arguments. adamc@173: adamc@125: Axiom ext_eq : forall (A : Type) (B : A -> Type) adamc@125: (f g : forall x, B x), adamc@125: (forall x, f x = g x) adamc@125: -> f = g. adamc@125: adamc@173: Theorem ext_eq_Set : forall (A : Set) (B : A -> Set) adamc@173: (f g : forall x, B x), adamc@173: (forall x, f x = g x) adamc@173: -> f = g. adamc@173: intros. adamc@173: rewrite (ext_eq _ _ _ H); reflexivity. adamc@173: Qed. adamc@173: adamc@173: Theorem ext_eq_forall : forall (A : Type) adamc@173: (f g : A -> Set), adamc@173: (forall x, f x = g x) adamc@173: -> @eq Type (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); intro.