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@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@125: Ltac ext_eq := apply ext_eq; intro.