Mercurial > cpdt > repo
diff src/Axioms.v @ 173:7fd470d8a788
System F
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 09 Nov 2008 15:15:41 -0500 |
parents | 8a548a6c7074 |
children | 094bd1e353dd |
line wrap: on
line diff
--- a/src/Axioms.v Sun Nov 09 14:24:31 2008 -0500 +++ b/src/Axioms.v Sun Nov 09 15:15:41 2008 -0500 @@ -9,9 +9,28 @@ (* Additional axioms not in the Coq standard library *) +Set Implicit Arguments. + Axiom ext_eq : forall (A : Type) (B : A -> Type) (f g : forall x, B x), (forall x, f x = g x) -> f = g. -Ltac ext_eq := apply ext_eq; intro. +Theorem ext_eq_Set : forall (A : Set) (B : A -> Set) + (f g : forall x, B x), + (forall x, f x = g x) + -> f = g. + intros. + rewrite (ext_eq _ _ _ H); reflexivity. +Qed. + +Theorem ext_eq_forall : forall (A : Type) + (f g : A -> Set), + (forall x, f x = g x) + -> @eq Type (forall x, f x) (forall x, g x). + intros. + rewrite (ext_eq _ _ _ H); trivial. +Qed. + +Ltac ext_eq := (apply ext_eq || apply ext_eq_Set + || apply ext_eq_forall); intro.