diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-12 19:34:46 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-12 19:34:46 +0000 |
| commit | e95cfce6398e41f0150aa6340bf8bc37eb66799f (patch) | |
| tree | 5adc9ead3af599f3188c3c02ecafa098b098f23b /theories/Init | |
| parent | 69380c8e0af2b4e4bc4767fa88bb37ebe2f2a7a9 (diff) | |
Ajout lemme projections
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4883 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init')
| -rwxr-xr-x | theories/Init/Datatypes.v | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 72758ffe0..d93bbbac1 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -92,9 +92,16 @@ Notation Snd := (snd ? ?). ]. Hints Resolve pair inl inr : core v62. -Lemma surjective_pairing : (A,B:Set;H:A*B)H=(pair A B (Fst H) (Snd H)). +Lemma surjective_pairing : (A,B:Set;p:A*B)p=(pair A B (Fst p) (Snd p)). Proof. -NewDestruct H; Reflexivity. +NewDestruct p; Reflexivity. +Qed. + +Lemma injective_projections : + (A,B:Set;p1,p2:A*B)(Fst p1)=(Fst p2)->(Snd p1)=(Snd p2)->p1=p2. +Proof. +NewDestruct p1; NewDestruct p2; Simpl; Intros Hfst Hsnd. +Rewrite Hfst; Rewrite Hsnd; Reflexivity. Qed. V7only[ |