diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-25 12:18:36 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-25 12:18:36 +0000 |
| commit | 4b0f28073b3db03d1991c680be99aedbb45de225 (patch) | |
| tree | ccec1722351608b1422eae824b856f0fcf186403 /test-suite/success/cc.v | |
| parent | bc8123f6b8f81fb3f2b1e03a832263fb0c4e70e1 (diff) | |
CC: added injection theory
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4987 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/cc.v')
| -rw-r--r-- | test-suite/success/cc.v | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index 881d6f9e5..18a99056b 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -1,6 +1,5 @@ Require CC. - Theorem t1: (A:Set)(a:A)(f:A->A) (f a)=a->(f (f a))=a. Intros. @@ -47,3 +46,16 @@ Theorem t4 : (A:Set; P:(A->Prop); u,v:A)u=v->(P u)->(P v). Intros. CCsolve. Save. + +(* Exambles with injection rule *) + +Theorem t5 : (A:Set;a,b,c,d:A)(a,c)=(b,d)->a=b/\c=d. +Intros. +Split;CC. +Save. + +Theorem t6 : (A:Set;a,c,d:A;f:A->A*A) (f=(pair A A a))->(f c)=(f d)->c=d. +Intros. +CC. +Save. + |