diff options
| author | letouzey | 2001-09-27 13:00:06 +0000 |
|---|---|---|
| committer | letouzey | 2001-09-27 13:00:06 +0000 |
| commit | ed97a490501de3693a8990b0f53deae43dba01a7 (patch) | |
| tree | a2e01e60ce52199830676b6016cdc193b08f1d1f | |
| parent | bf28565aeda18a454bb750658c94a1cc56f187c7 (diff) | |
and_rec redondant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2081 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rwxr-xr-x | theories/Init/Specif.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 7143f8a346..3bbb9ba7e2 100755 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -203,10 +203,12 @@ Proof. Apply (h2 h1). Qed. +(*i is now generated Theorem and_rec : (A,B:Prop)(C:Set)(A->B->C)->(A/\B)->C. Proof. Intros A B C F AB; Apply F; Elim AB; Auto. -Qed. +Qed. +i*) (*i is now a theorem Axiom eq_rec : (A:Set)(a:A)(P:A->Set)(P a)->(b:A) a=b -> (P b). |